- auto-generated mli files for future documentation

- new Makefiles to handle these mli

3 files changed, 84 insertions, 2 deletions

diff --git a/src/versions/native/Make b/src/versions/native/Make
index 07ff232..406ebb9 100644
--- a/src/versions/native/Make
+++ b/src/versions/native/Make
@@ -48,41 +48,62 @@ CAMLYACC = $(CAMLBIN)ocamlyacc
 
 versions/native/Structures.v
 versions/native/structures.ml
+versions/native/structures.mli
 
 trace/coqTerms.ml
+trace/coqTerms.mli
 trace/satAtom.ml
+trace/satAtom.mli
 trace/smtAtom.ml
 trace/smtAtom.mli
 trace/smtCertif.ml
+trace/smtCertif.mli
 trace/smtCnf.ml
+trace/smtCnf.mli
 trace/smtCommands.ml
+trace/smtCommands.mli
 trace/smtForm.ml
 trace/smtForm.mli
 trace/smtMisc.ml
+trace/smtMisc.mli
 trace/smtTrace.ml
+trace/smtTrace.mli
 
 smtlib2/smtlib2_parse.ml
+smtlib2/smtlib2_parse.mli
 smtlib2/smtlib2_lex.ml
+smtlib2/smtlib2_lex.mli
 smtlib2/smtlib2_ast.ml
+smtlib2/smtlib2_ast.mli
 smtlib2/smtlib2_genConstr.ml
+smtlib2/smtlib2_genConstr.mli
 smtlib2/smtlib2_util.ml
+smtlib2/smtlib2_util.mli
 
 verit/veritParser.ml
+verit/veritParser.mli
 verit/veritLexer.ml
+verit/veritLexer.mli
 verit/verit.ml
+verit/verit.mli
 verit/veritSyntax.ml
 verit/veritSyntax.mli
 
 zchaff/cnfParser.ml
+zchaff/cnfParser.mli
 zchaff/satParser.ml
+zchaff/satParser.mli
 zchaff/zchaff.ml
+zchaff/zchaff.mli
 zchaff/zchaffParser.ml
+zchaff/zchaffParser.mli
 
 cnf/Cnf.v
 
 euf/Euf.v
 
 lia/lia.ml
+lia/lia.mli
 lia/Lia.v
 
 spl/Assumptions.v
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
index bbeb95a..540b7ce 100644
--- a/src/versions/native/Makefile
+++ b/src/versions/native/Makefile
@@ -192,9 +192,30 @@ MLFILES:=lia/lia.ml\
 -include $(addsuffix .d,$(MLFILES))
 .SECONDARY: $(addsuffix .d,$(MLFILES))
 
-MLIFILES:=verit/veritSyntax.mli\
+MLIFILES:=lia/lia.mli\
+  zchaff/zchaffParser.mli\
+  zchaff/zchaff.mli\
+  zchaff/satParser.mli\
+  zchaff/cnfParser.mli\
+  verit/veritSyntax.mli\
+  verit/verit.mli\
+  verit/veritLexer.mli\
+  verit/veritParser.mli\
+  smtlib2/smtlib2_util.mli\
+  smtlib2/smtlib2_genConstr.mli\
+  smtlib2/smtlib2_ast.mli\
+  smtlib2/smtlib2_lex.mli\
+  smtlib2/smtlib2_parse.mli\
+  trace/smtTrace.mli\
+  trace/smtMisc.mli\
   trace/smtForm.mli\
-  trace/smtAtom.mli
+  trace/smtCommands.mli\
+  trace/smtCnf.mli\
+  trace/smtCertif.mli\
+  trace/smtAtom.mli\
+  trace/satAtom.mli\
+  trace/coqTerms.mli\
+  versions/native/structures.mli
 
 -include $(addsuffix .d,$(MLIFILES))
 .SECONDARY: $(addsuffix .d,$(MLIFILES))
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
new file mode 100644
index 0000000..057625c
--- /dev/null
+++ b/src/versions/native/structures.mli
@@ -0,0 +1,40 @@
+val gen_constant : string list list -> string -> Term.constr lazy_t
+val int63_modules : string list list
+val mkInt : int -> Term.constr
+val cint : Term.constr lazy_t
+val parray_modules : string list list
+val max_array_size : int
+val mkArray : Term.types * Term.constr array -> Term.constr
+val mkTrace :
+  ('a -> Term.constr) ->
+  ('a -> 'a) ->
+  Term.constr Lazy.t ->
+  'b ->
+  'c -> 'd -> 'e -> int -> Term.types -> Term.constr -> 'a ref -> Term.constr
+type names_id_t = Names.identifier
+val dummy_loc : Pp.loc
+val mkUConst : Term.constr -> Entries.definition_entry
+val mkTConst : Term.constr -> 'a -> Term.types -> Entries.definition_entry
+val error : string -> 'a
+val coqtype : Term.types lazy_t
+val declare_new_type : Names.variable -> Term.constr
+val declare_new_variable : Names.variable -> Term.types -> Term.constr
+val extern_constr : Term.constr -> Topconstr.constr_expr
+val vernacentries_interp : Topconstr.constr_expr -> unit
+val pr_constr_env : Environ.env -> Term.constr -> Pp.std_ppcmds
+val lift : int -> Term.constr -> Term.constr
+val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
+val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
+val assert_before : Names.name -> Term.types -> Proof_type.tactic
+val vm_cast_no_check : Term.constr -> Proof_type.tactic
+val mk_tactic :
+  (Environ.env ->
+   Evd.evar_map -> Term.types -> Proof_type.goal Tacmach.sigma -> 'a) ->
+  Proof_type.goal Tacmach.sigma -> 'a
+val set_evars_tac : 'a -> Proof_type.tactic
+val ppconstr_lsimpleconstr : Ppconstr.precedence
+val constrextern_extern_constr : Term.constr -> Topconstr.constr_expr
+module Micromega_plugin_Certificate = Certificate
+module Micromega_plugin_Coq_micromega = Coq_micromega
+module Micromega_plugin_Micromega = Micromega
+module Micromega_plugin_Mutils = Mutils