Extract.v
Require Extraction.
Require Termes.
Require Conv.
Require Types.
Require Conv_Dec.
Require Infer.
Require Names.
Require Expr.
Require Machine.
Write Caml File "core" [
list_index is_free_var
check_typ red_to_sort red_to_prod exec_axiom
glob_ctx glob_names empty_state
name_dec find_free_var
synthesis interp_command transl_message transl_error interp_ast].
07/03/97, 14:41