ExtractV6Beta.v
Require MlExtract.
Require CoqV6Beta.
Write Caml File "kernel" [
v6_is_subtype_dec
cts_prim_algos
(* algos generaux a ne pas expanser *)
is_a_sort cumul_least_sort cumul_least_prod
(* algos specifiques ecc *)
calc_dec v6_sort_dec v6_inf_rule v6_inf_axiom (*ecc_algorithms*)
(* acces aux champs des records *)
pa_infer_axiom pa_infer_rule
pa_lift pa_subst pa_least_sort pa_least_prod pa_le_type_dec
scts_whnf scts_convert_hn scts_rt_univ_dec
(* NE PAS EXPANSER: *)
full_ppal_type (*full_type_checker*)
(* OBLIGATOIRE: interface noyau *)
env_v6 check_type infer_type check_wf_type add_type add_def
sort_of_gen gen_of_sort
]
(*[
Acc3_rec
v6_algorithms full_cts_type_checker full_type_checker
]*)
.
23/12/98, 14:29