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