mise en place fichiers extraction

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1397 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 90 insertions, 0 deletions

diff --git a/contrib/extraction/mlimport.mli b/contrib/extraction/mlimport.mli
new file mode 100644
index 000000000..ac32f5139
--- /dev/null
+++ b/contrib/extraction/mlimport.mli
@@ -0,0 +1,90 @@
+
+(*i $Id$ i*)
+
+open Names
+open Term
+
+val is_ml_import : global_reference -> bool
+val find_ml_import : global_reference -> identifier
+
+val find_ml_extract : global_reference -> identifier
+val is_ml_extract : global_reference -> bool
+
+(*
+val list0n : int -> int list
+val next_global_ident : Names.identifier -> Names.identifier
+val ml_import_tab : (Term.sorts Term.oper, Names.identifier) Hashtabl.t
+val mL_INDUCTIVES : Names.section_path list ref
+val add_ml_inductive_import : Names.section_path -> unit
+val add_ml_import : Term.sorts Term.oper -> Names.identifier -> unit
+val sp_is_ml_import : Names.section_path -> bool
+val sp_prod : Names.section_path
+val sp_is_ml_import_or_prod : Names.section_path -> bool
+val inMLImport : Term.sorts Term.oper * Names.identifier -> Libobject.obj
+val outMLImport : Libobject.obj -> Term.sorts Term.oper * Names.identifier
+val ml_extract_tab : (Term.sorts Term.oper, Names.identifier) Hashtabl.t
+val add_ml_extract : Term.sorts Term.oper -> Names.identifier -> unit
+val sp_is_ml_extract : Names.section_path -> bool
+val inMLExtract : Term.sorts Term.oper * Names.identifier -> Libobject.obj
+val outMLExtract : Libobject.obj -> Term.sorts Term.oper * Names.identifier
+val is_import_or_extract : Names.section_path -> bool
+val freeze :
+  unit ->
+  (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t *
+  Names.section_path list *
+  (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t
+val unfreeze :
+  (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t *
+  Names.section_path list *
+  (Term.sorts Term.oper, Names.identifier) Hashtabl.frozen_t -> unit
+val whd_fwify : 'a Term.oper Generic.term -> 'a Term.oper Generic.term
+val fwify : Reduction.reduction_function
+val fwsp_of_id : Names.identifier -> Names.section_path
+val make_fw_parameter_body :
+  Term.type_judgement Names.signature * Term.type_judgement ->
+  Constrtypes.constant_body
+val fw_infexecute_parameter :
+  Term.context ->
+  Names.identifier ->
+  Term.constr ->
+  Impuniv.universes * (Names.path_kind * Constrtypes.constant_body) list
+val fw_machine_parameter :
+  Term.context -> Names.identifier * Term.constr -> unit
+val fw_parameter : Names.identifier -> CoqAst.t -> unit
+val ml_import : Names.identifier -> Names.identifier -> CoqAst.t -> unit
+val id_of_varg : Vernacinterp.vernac_arg -> Names.identifier
+val not_an_axiom : Names.identifier -> 'a
+val not_have_type :
+  Term.environment ->
+  Constrtypes.constant_body -> Constrtypes.constant_body -> 'a
+val fw_infexecute_constant :
+  Term.context ->
+  Names.identifier ->
+  Term.constr ->
+  Impuniv.universes * (Names.path_kind * Constrtypes.constant_body) list
+val fw_link : Names.identifier -> CoqAst.t -> unit
+val fw_machine_minductive :
+  Term.context ->
+  int ->
+  (Names.identifier * Names.name * Term.type_judgement * Term.constr *
+   Names.identifier array)
+  array -> bool -> unit
+val fw_fconstruct :
+  'a Evd.evar_map -> Term.context -> CoqAst.t -> Term.type_judgement
+val fw_build_mutual :
+  (Names.identifier * CoqAst.t) list ->
+  (Names.identifier * CoqAst.t * (Names.identifier * CoqAst.t) list) list ->
+  bool -> unit
+val not_same_number_types : unit -> 'a
+val not_same_number_constructors : Names.identifier * Names.identifier -> 'a
+val ml_import_inductive :
+  (Names.identifier * Names.identifier list) list ->
+  (Names.identifier * CoqAst.t) list ->
+  (Names.identifier * CoqAst.t * (Names.identifier * CoqAst.t) list) list ->
+  bool -> unit
+val extract_constant : Names.identifier -> Names.identifier -> unit
+val extract_inductive :
+  Names.identifier -> Names.identifier * Names.identifier list -> unit
+val fprint_recipe : Constrtypes.recipe ref option -> Pp.std_ppcmds
+val fprint_name : Names.identifier -> Pp.std_ppcmds
+*)