ExtractECC.v

Require MlExtract.
Require ECC.

Write Caml File "kernel" [
ecc_is_subtype_dec
cts_prim_algos

not_topsort typ_of_decl

(* algos generaux a ne pas expanser *)
is_a_sort cumul_least_sort cumul_least_prod

(* algos specifiques ecc *)
calc_dec ecc_sort_dec ecc_inf_rule ecc_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_ecc check_type infer_type check_wf_type add_type add_def
sort_of_gen gen_of_sort
]
(*[ Acc3_rec ecc_algorithms full_cts_type_checker full_type_checker ]*)
.

23/12/98, 14:29