- auto-generated mli files for future documentation

- new Makefiles to handle these mli

24 files changed, 1007 insertions, 6 deletions

diff --git a/src/extraction/Makefile b/src/extraction/Makefile
index 043afa1..73b0ae4 100644
--- a/src/extraction/Makefile
+++ b/src/extraction/Makefile
@@ -1,6 +1,6 @@
 # List of user's files and name of the final program (edit this part)
 
-USERFILES=smtcoq.ml
+USERFILES=smtcoq.ml smtcoq.mli
 PROGRAM=smtcoq
 # USERFILES=test.ml
 # PROGRAM=test
@@ -19,9 +19,12 @@ SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../
 COQLIB=-I ${COQTOP}kernel -I ${COQTOP}lib -I ${COQTOP}library -I ${COQTOP}parsing -I ${COQTOP}pretyping -I ${COQTOP}interp -I ${COQTOP}proofs -I ${COQTOP}tactics -I ${COQTOP}toplevel -I ${COQTOP}plugins/btauto -I ${COQTOP}plugins/cc -I ${COQTOP}plugins/decl_mode -I ${COQTOP}plugins/extraction -I ${COQTOP}plugins/field -I ${COQTOP}plugins/firstorder -I ${COQTOP}plugins/fourier -I ${COQTOP}plugins/funind -I ${COQTOP}plugins/micromega -I ${COQTOP}plugins/nsatz -I ${COQTOP}plugins/omega -I ${COQTOP}plugins/quote -I ${COQTOP}plugins/ring -I ${COQTOP}plugins/romega -I ${COQTOP}plugins/rtauto -I ${COQTOP}plugins/setoid_ring -I ${COQTOP}plugins/syntax -I ${COQTOP}plugins/xml -I /usr/lib/ocaml/camlp5
 
 CMXA=nums.cmxa str.cmxa unix.cmxa gramlib.cmxa dynlink.cmxa ${COQTOP}kernel/byterun/coq_fix_code.o ${COQTOP}kernel/byterun/coq_interp.o ${COQTOP}kernel/byterun/coq_memory.o ${COQTOP}kernel/byterun/coq_values.o clib.cmxa lib.cmxa kernel.cmxa library.cmxa pretyping.cmxa interp.cmxa proofs.cmxa parsing.cmxa tactics.cmxa toplevel.cmxa micromega_plugin.cmxa smtcoq.cmxa
-CMI=extrNative.cmi sat_checker.cmi smt_checker.cmi
+CMI=extrNative.cmi sat_checker.cmi zchaff_checker.cmi smt_checker.cmi verit_checker.cmi
 CMX=extrNative.cmx sat_checker.cmx zchaff_checker.cmx smt_checker.cmx verit_checker.cmx
-USERCMX=$(USERFILES:.ml=.cmx)
+USERML=$(filter %.ml,$(USERFILES))
+USERCMX=$(USERML:%.ml=%.cmx)
+USERMLI=$(filter %.mli,$(USERFILES))
+USERCMI=$(USERMLI:%.mli=%.cmi)
 
 OCAMLC=ocamlc
 OCAMLOPT=ocamlopt
@@ -35,7 +38,7 @@ all: $(PROGRAM)
 %.cmx: %.ml
 	$(OCAMLOPT) -c $(FLAGS) $(SMTLIB) $(COQLIB) $<
 
-$(PROGRAM): $(CMI) $(CMX) $(USERCMX)
+$(PROGRAM): $(CMI) $(CMX) $(USERCMI) $(USERCMX)
 	$(OCAMLOPT) $(FLAGS) $(SMTLIB) $(COQLIB) -o $@ $(COMPILEFLAGS) $(CMXA) $(CMX) $(USERCMX)
 
 
diff --git a/src/extraction/smtcoq.mli b/src/extraction/smtcoq.mli
new file mode 100644
index 0000000..7b33e0f
--- /dev/null
+++ b/src/extraction/smtcoq.mli
@@ -0,0 +1,5 @@
+type solver = Zchaff | Verit
+val usage : string
+val string_of_solver : solver -> string
+val verifier_of_solver : solver -> string -> string -> bool
+val run : solver -> string -> string -> unit
diff --git a/src/extraction/test.mli b/src/extraction/test.mli
new file mode 100644
index 0000000..8b13789
--- /dev/null
+++ b/src/extraction/test.mli
@@ -0,0 +1 @@
+
diff --git a/src/extraction/verit_checker.mli b/src/extraction/verit_checker.mli
new file mode 100644
index 0000000..3c43d22
--- /dev/null
+++ b/src/extraction/verit_checker.mli
@@ -0,0 +1,45 @@
+module Mc = Structures.Micromega_plugin_Certificate.Mc
+val mkInt : int -> ExtrNative.uint
+val mkArray : 'a array -> 'a ExtrNative.parray
+val dump_nat : Mc.nat -> Smt_checker.nat
+val dump_positive : Mc.positive -> Smt_checker.positive
+val dump_z : Mc.z -> Smt_checker.z
+val dump_pol : Mc.z Mc.pol -> Smt_checker.z Smt_checker.pol
+val dump_psatz : Mc.z Mc.psatz -> Smt_checker.z Smt_checker.psatz
+val dump_list : ('a -> 'b) -> 'a list -> 'b Smt_checker.list
+val dump_proof_term : Micromega.zArithProof -> Smt_checker.zArithProof
+val to_coq :
+  ('a -> Smt_checker.int) ->
+  'a SmtCertif.clause ->
+  Smt_checker.Euf_Checker.step ExtrNative.parray ExtrNative.parray *
+  'a SmtCertif.clause
+val btype_to_coq : SmtAtom.btype -> Smt_checker.Typ.coq_type
+val c_to_coq : SmtAtom.cop -> Smt_checker.Atom.cop
+val u_to_coq : SmtAtom.uop -> Smt_checker.Atom.unop
+val b_to_coq : SmtAtom.bop -> Smt_checker.Atom.binop
+val n_to_coq : SmtAtom.nop -> Smt_checker.Typ.coq_type
+val i_to_coq : SmtAtom.indexed_op -> ExtrNative.uint
+val a_to_coq : SmtAtom.atom -> Smt_checker.Atom.atom
+val atom_interp_tbl :
+  SmtAtom.Atom.reify_tbl -> Smt_checker.Atom.atom ExtrNative.parray
+val form_to_coq : SmtAtom.Form.t -> ExtrNative.uint
+val args_to_coq : SmtAtom.Form.t array -> ExtrNative.uint ExtrNative.parray
+val pf_to_coq :
+  (SmtAtom.hatom, SmtAtom.Form.t) SmtForm.gen_pform -> Smt_checker.Form.form
+val form_interp_tbl :
+  SmtAtom.Form.reify -> Smt_checker.Form.form ExtrNative.parray
+val count_btype : int ref
+val count_op : int ref
+val declare_sort : Smtlib2_ast.symbol -> SmtAtom.btype
+val declare_fun :
+  Smtlib2_ast.symbol ->
+  Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op
+val declare_commands :
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  SmtAtom.Form.t list -> Smtlib2_ast.command -> SmtAtom.Form.t list
+val import_smtlib2 :
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify -> string -> SmtAtom.Form.t list
+val this_clear_all : unit -> unit
+val checker : string -> string -> bool
diff --git a/src/extraction/zchaff_checker.mli b/src/extraction/zchaff_checker.mli
new file mode 100644
index 0000000..d24a1e3
--- /dev/null
+++ b/src/extraction/zchaff_checker.mli
@@ -0,0 +1,13 @@
+val mkInt : int -> ExtrNative.uint
+val mkArray : 'a array -> 'a ExtrNative.parray
+val make_roots :
+  SatAtom.Form.t SmtCertif.clause ->
+  'a SmtCertif.clause -> ExtrNative.uint ExtrNative.parray ExtrNative.parray
+val to_coq :
+  'a ->
+  'b * 'c * 'd * 'e * 'f * 'g * 'h * 'i * 'j * 'k * 'l * 'm * 'n * 'o * 'p *
+  'q * 'r * 's * 't ->
+  'u SmtCertif.clause ->
+  Sat_checker.Sat_Checker.step ExtrNative.parray ExtrNative.parray *
+  'u SmtCertif.clause
+val checker : string -> string -> bool
diff --git a/src/lia/lia.mli b/src/lia/lia.mli
new file mode 100644
index 0000000..bb5587f
--- /dev/null
+++ b/src/lia/lia.mli
@@ -0,0 +1,59 @@
+val pos_of_int : int -> Structures.Micromega_plugin_Micromega.positive
+val z_of_int : int -> Structures.Micromega_plugin_Micromega.z
+type my_tbl = { tbl : (SmtAtom.hatom, int) Hashtbl.t; mutable count : int; }
+val get_atom_var : my_tbl -> SmtAtom.hatom -> int
+val create_tbl : int -> my_tbl
+val smt_Atom_to_micromega_pos :
+  SmtAtom.hatom -> Structures.Micromega_plugin_Micromega.positive
+val smt_Atom_to_micromega_Z :
+  SmtAtom.hatom -> Structures.Micromega_plugin_Micromega.z
+val smt_Atom_to_micromega_pExpr :
+  my_tbl ->
+  SmtAtom.hatom ->
+  Structures.Micromega_plugin_Micromega.z
+  Structures.Micromega_plugin_Micromega.pExpr
+val smt_binop_to_micromega_formula :
+  my_tbl ->
+  SmtAtom.bop ->
+  SmtAtom.hatom ->
+  SmtAtom.hatom ->
+  Structures.Micromega_plugin_Micromega.z
+  Structures.Micromega_plugin_Micromega.formula
+val smt_Atom_to_micromega_formula :
+  my_tbl ->
+  SmtAtom.hatom ->
+  Structures.Micromega_plugin_Micromega.z
+  Structures.Micromega_plugin_Micromega.formula
+val default_constr : Term.constr
+val default_tag : Structures.Micromega_plugin_Mutils.Tag.t
+val binop_array :
+  ('a -> 'b -> 'c) -> 'a -> ('c -> 'c -> 'c) -> 'c -> 'b array -> 'c
+val smt_Form_to_coq_micromega_formula :
+  my_tbl ->
+  SmtAtom.Form.t ->
+  Structures.Micromega_plugin_Micromega.z
+  Structures.Micromega_plugin_Coq_micromega.formula
+val binop_list :
+  my_tbl ->
+  (Structures.Micromega_plugin_Micromega.z
+   Structures.Micromega_plugin_Coq_micromega.formula ->
+   Structures.Micromega_plugin_Micromega.z
+   Structures.Micromega_plugin_Coq_micromega.formula ->
+   Structures.Micromega_plugin_Micromega.z
+   Structures.Micromega_plugin_Coq_micromega.formula) ->
+  Structures.Micromega_plugin_Micromega.z
+  Structures.Micromega_plugin_Coq_micromega.formula ->
+  SmtAtom.Form.t list ->
+  Structures.Micromega_plugin_Micromega.z
+  Structures.Micromega_plugin_Coq_micromega.formula
+val smt_clause_to_coq_micromega_formula :
+  my_tbl ->
+  SmtAtom.Form.t list ->
+  Structures.Micromega_plugin_Micromega.z
+  Structures.Micromega_plugin_Coq_micromega.formula
+val build_lia_certif :
+  SmtAtom.Form.t list ->
+  my_tbl *
+  Structures.Micromega_plugin_Micromega.z
+  Structures.Micromega_plugin_Coq_micromega.formula *
+  Certificate.Mc.zArithProof list option
diff --git a/src/smtlib2/smtlib2_ast.mli b/src/smtlib2/smtlib2_ast.mli
new file mode 100644
index 0000000..4fb1280
--- /dev/null
+++ b/src/smtlib2/smtlib2_ast.mli
@@ -0,0 +1,79 @@
+type loc = Lexing.position * Lexing.position
+type specconstant =
+    SpecConstsDec of loc * string
+  | SpecConstNum of loc * string
+  | SpecConstString of loc * string
+  | SpecConstsHex of loc * string
+  | SpecConstsBinary of loc * string
+type symbol = Symbol of loc * string | SymbolWithOr of loc * string
+type sexpr =
+    SexprSpecConst of loc * specconstant
+  | SexprSymbol of loc * symbol
+  | SexprKeyword of loc * string
+  | SexprInParen of loc * (loc * sexpr list)
+type attributevalue =
+    AttributeValSpecConst of loc * specconstant
+  | AttributeValSymbol of loc * symbol
+  | AttributeValSexpr of loc * (loc * sexpr list)
+type attribute =
+    AttributeKeyword of loc * string
+  | AttributeKeywordValue of loc * string * attributevalue
+type an_option = AnOptionAttribute of loc * attribute
+type infoflag = InfoFlagKeyword of loc * string
+type identifier =
+    IdSymbol of loc * symbol
+  | IdUnderscoreSymNum of loc * symbol * (loc * string list)
+type sort =
+    SortIdentifier of loc * identifier
+  | SortIdSortMulti of loc * identifier * (loc * sort list)
+type qualidentifier =
+    QualIdentifierId of loc * identifier
+  | QualIdentifierAs of loc * identifier * sort
+type sortedvar = SortedVarSymSort of loc * symbol * sort
+type varbinding = VarBindingSymTerm of loc * symbol * term
+and term =
+    TermSpecConst of loc * specconstant
+  | TermQualIdentifier of loc * qualidentifier
+  | TermQualIdTerm of loc * qualidentifier * (loc * term list)
+  | TermLetTerm of loc * (loc * varbinding list) * term
+  | TermForAllTerm of loc * (loc * sortedvar list) * term
+  | TermExistsTerm of loc * (loc * sortedvar list) * term
+  | TermExclimationPt of loc * term * (loc * attribute list)
+type command =
+    CSetLogic of loc * symbol
+  | CSetOption of loc * an_option
+  | CSetInfo of loc * attribute
+  | CDeclareSort of loc * symbol * string
+  | CDefineSort of loc * symbol * (loc * symbol list) * sort
+  | CDeclareFun of loc * symbol * (loc * sort list) * sort
+  | CDefineFun of loc * symbol * (loc * sortedvar list) * sort * term
+  | CPush of loc * string
+  | CPop of loc * string
+  | CAssert of loc * term
+  | CCheckSat of loc
+  | CGetAssert of loc
+  | CGetProof of loc
+  | CGetUnsatCore of loc
+  | CGetValue of loc * (loc * term list)
+  | CGetAssign of loc
+  | CGetOption of loc * string
+  | CGetInfo of loc * infoflag
+  | CExit of loc
+type commands = Commands of loc * (loc * command list)
+val loc_an_option : an_option -> loc
+val loc_attribute : attribute -> loc
+val loc_attributevalue : attributevalue -> loc
+val loc_command : command -> loc
+val loc_commands : commands -> loc
+val loc_identifier : identifier -> loc
+val loc_infoflag : infoflag -> loc
+val loc_qualidentifier : qualidentifier -> loc
+val loc_sexpr : sexpr -> loc
+val loc_sort : sort -> loc
+val loc_sortedvar : sortedvar -> loc
+val loc_specconstant : specconstant -> loc
+val loc_symbol : symbol -> loc
+val loc_term : term -> loc
+val loc_varbinding : varbinding -> loc
+val loc_couple : 'a * 'b -> 'a
+val loc_of : commands -> loc
diff --git a/src/smtlib2/smtlib2_genConstr.mli b/src/smtlib2/smtlib2_genConstr.mli
new file mode 100644
index 0000000..ba69741
--- /dev/null
+++ b/src/smtlib2/smtlib2_genConstr.mli
@@ -0,0 +1,34 @@
+val pp_symbol : Smtlib2_ast.symbol -> string
+val string_of_symbol : Smtlib2_ast.symbol -> string
+val identifier_of_qualidentifier :
+  Smtlib2_ast.qualidentifier -> Smtlib2_ast.identifier
+val string_type : string -> SmtAtom.btype
+val sort_of_string : string -> SmtAtom.btype * 'a list
+val sort_of_symbol : Smtlib2_ast.symbol -> SmtAtom.btype * 'a list
+val string_of_identifier : Smtlib2_ast.identifier -> string
+val string_of_qualidentifier : Smtlib2_ast.qualidentifier -> string
+val sort_of_sort : Smtlib2_ast.sort -> (SmtAtom.btype * 'a list as 'a)
+val declare_sort :
+  SmtAtom.Btype.reify_tbl -> Smtlib2_ast.symbol -> SmtAtom.btype
+val declare_fun :
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  Smtlib2_ast.symbol ->
+  Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op
+val make_root_specconstant :
+  SmtAtom.Atom.reify_tbl -> Smtlib2_ast.specconstant -> SmtAtom.hatom
+type atom_form = Atom of SmtAtom.Atom.t | Form of SmtAtom.Form.t
+val make_root :
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify -> Smtlib2_ast.term -> SmtAtom.Form.t
+val declare_commands :
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  SmtAtom.Form.t list -> Smtlib2_ast.command -> SmtAtom.Form.t list
+val import_smtlib2 :
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify -> string -> SmtAtom.Form.t list
diff --git a/src/smtlib2/smtlib2_util.mli b/src/smtlib2/smtlib2_util.mli
new file mode 100644
index 0000000..8afbce3
--- /dev/null
+++ b/src/smtlib2/smtlib2_util.mli
@@ -0,0 +1,8 @@
+type extradata = unit
+val initial_data : unit -> unit
+val file : string ref
+val line : int ref
+type pos = int
+val string_of_pos : int -> string
+val cur_pd : unit -> int * unit
+type pd = pos * extradata
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
new file mode 100644
index 0000000..8fd166e
--- /dev/null
+++ b/src/trace/coqTerms.mli
@@ -0,0 +1,112 @@
+val gen_constant : string list list -> string -> Term.constr lazy_t
+val cint : Term.constr lazy_t
+val ceq63 : Term.constr lazy_t
+val carray : Term.constr lazy_t
+val positive_modules : string list list
+val cpositive : Term.constr lazy_t
+val cxI : Term.constr lazy_t
+val cxO : Term.constr lazy_t
+val cxH : Term.constr lazy_t
+val ceqbP : Term.constr lazy_t
+val z_modules : string list list
+val cZ : Term.constr lazy_t
+val cZ0 : Term.constr lazy_t
+val cZpos : Term.constr lazy_t
+val cZneg : Term.constr lazy_t
+val copp : Term.constr lazy_t
+val cadd : Term.constr lazy_t
+val csub : Term.constr lazy_t
+val cmul : Term.constr lazy_t
+val cltb : Term.constr lazy_t
+val cleb : Term.constr lazy_t
+val cgeb : Term.constr lazy_t
+val cgtb : Term.constr lazy_t
+val ceqbZ : Term.constr lazy_t
+val bool_modules : string list list
+val cbool : Term.constr lazy_t
+val ctrue : Term.constr lazy_t
+val cfalse : Term.constr lazy_t
+val candb : Term.constr lazy_t
+val corb : Term.constr lazy_t
+val cxorb : Term.constr lazy_t
+val cnegb : Term.constr lazy_t
+val cimplb : Term.constr lazy_t
+val ceqb : Term.constr lazy_t
+val cifb : Term.constr lazy_t
+val creflect : Term.constr lazy_t
+val clist : Term.constr lazy_t
+val cnil : Term.constr lazy_t
+val ccons : Term.constr lazy_t
+val coption : Term.constr lazy_t
+val cSome : Term.constr lazy_t
+val cNone : Term.constr lazy_t
+val cpair : Term.constr lazy_t
+val csigT : Term.constr lazy_t
+val cnot : Term.constr lazy_t
+val ceq : Term.constr lazy_t
+val crefl_equal : Term.constr lazy_t
+val smt_modules : string list list
+val cState_C_t : Term.constr lazy_t
+val cdistinct : Term.constr lazy_t
+val ctype : Term.constr lazy_t
+val cTZ : Term.constr lazy_t
+val cTbool : Term.constr lazy_t
+val cTpositive : Term.constr lazy_t
+val cTindex : Term.constr lazy_t
+val ctyp_eqb : Term.constr lazy_t
+val cTyp_eqb : Term.constr lazy_t
+val cte_carrier : Term.constr lazy_t
+val cte_eqb : Term.constr lazy_t
+val ctyp_eqb_of_typ_eqb_param : Term.constr lazy_t
+val cunit_typ_eqb : Term.constr lazy_t
+val ctval : Term.constr lazy_t
+val cTval : Term.constr lazy_t
+val cCO_xH : Term.constr lazy_t
+val cCO_Z0 : Term.constr lazy_t
+val cUO_xO : Term.constr lazy_t
+val cUO_xI : Term.constr lazy_t
+val cUO_Zpos : Term.constr lazy_t
+val cUO_Zneg : Term.constr lazy_t
+val cUO_Zopp : Term.constr lazy_t
+val cBO_Zplus : Term.constr lazy_t
+val cBO_Zminus : Term.constr lazy_t
+val cBO_Zmult : Term.constr lazy_t
+val cBO_Zlt : Term.constr lazy_t
+val cBO_Zle : Term.constr lazy_t
+val cBO_Zge : Term.constr lazy_t
+val cBO_Zgt : Term.constr lazy_t
+val cBO_eq : Term.constr lazy_t
+val cNO_distinct : Term.constr lazy_t
+val catom : Term.constr lazy_t
+val cAcop : Term.constr lazy_t
+val cAuop : Term.constr lazy_t
+val cAbop : Term.constr lazy_t
+val cAnop : Term.constr lazy_t
+val cAapp : Term.constr lazy_t
+val cform : Term.constr lazy_t
+val cFatom : Term.constr lazy_t
+val cFtrue : Term.constr lazy_t
+val cFfalse : Term.constr lazy_t
+val cFnot2 : Term.constr lazy_t
+val cFand : Term.constr lazy_t
+val cFor : Term.constr lazy_t
+val cFxor : Term.constr lazy_t
+val cFimp : Term.constr lazy_t
+val cFiff : Term.constr lazy_t
+val cFite : Term.constr lazy_t
+val cis_true : Term.constr lazy_t
+val cvalid_sat_checker : Term.constr lazy_t
+val cinterp_var_sat_checker : Term.constr lazy_t
+val make_certif_ops :
+  string list list ->
+  Term.constr array option ->
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t
+val ceq_refl_true : Term.constr lazy_t
+val eq_refl_true : unit -> Term.constr
+val vm_cast_true : Term.constr -> Term.constr
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
new file mode 100644
index 0000000..5d4201b
--- /dev/null
+++ b/src/trace/satAtom.mli
@@ -0,0 +1,112 @@
+module Atom :
+  sig
+    type t = int
+    val index : 'a -> 'a
+    val equal : 'a -> 'a -> bool
+    val is_bool_type : 'a -> bool
+    type reify_tbl = {
+      mutable count : int;
+      tbl : (Term.constr, int) Hashtbl.t;
+    }
+    val create : unit -> reify_tbl
+    val declare : reify_tbl -> Term.constr -> int
+    val get : reify_tbl -> Term.constr -> int
+    val atom_tbl : reify_tbl -> Term.constr array
+    val interp_tbl : reify_tbl -> Term.constr
+  end
+module Form :
+  sig
+    type hatom = Atom.t
+    type t = SmtForm.Make(Atom).t
+    type pform = (hatom, t) SmtForm.gen_pform
+    val pform_true : pform
+    val pform_false : pform
+    val equal : t -> t -> bool
+    val to_lit : t -> int
+    val index : t -> int
+    val pform : t -> pform
+    val neg : t -> t
+    val is_pos : t -> bool
+    val is_neg : t -> bool
+    val to_smt :
+      (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
+    exception NotWellTyped of pform
+    type reify = SmtForm.Make(Atom).reify
+    val create : unit -> reify
+    val clear : reify -> unit
+    val get : reify -> pform -> t
+    val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+    val flatten : reify -> t -> t
+    val to_coq : t -> Term.constr
+    val pform_tbl : reify -> pform array
+    val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
+    val interp_tbl : reify -> Term.constr * Term.constr
+    val nvars : reify -> int
+    val interp_to_coq :
+      (hatom -> Term.constr) ->
+      (int, Term.constr) Hashtbl.t -> t -> Term.constr
+  end
+module Trace :
+  sig
+    val share_value : Form.t SmtCertif.clause -> unit
+    module HashedHeadRes :
+      sig
+        type t = Form.t SmtCertif.resolution
+        val equal :
+          'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool
+        val hash : 'a SmtCertif.resolution -> int
+      end
+    module HRtbl :
+      sig
+        type key = HashedHeadRes.t
+        type 'a t = 'a Hashtbl.Make(HashedHeadRes).t
+        val create : int -> 'a t
+        val clear : 'a t -> unit
+        val reset : 'a t -> unit
+        val copy : 'a t -> 'a t
+        val add : 'a t -> key -> 'a -> unit
+        val remove : 'a t -> key -> unit
+        val find : 'a t -> key -> 'a
+        val find_all : 'a t -> key -> 'a list
+        val replace : 'a t -> key -> 'a -> unit
+        val mem : 'a t -> key -> bool
+        val iter : (key -> 'a -> unit) -> 'a t -> unit
+        val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+        val length : 'a t -> int
+        val stats : 'a t -> Hashtbl.statistics
+      end
+    val common_head :
+      'a SmtCertif.clause list ->
+      'b SmtCertif.clause list ->
+      'a SmtCertif.clause list * 'a SmtCertif.clause list *
+      'b SmtCertif.clause list
+    val share_prefix : Form.t SmtCertif.clause -> int -> unit
+  end
+module Cnf :
+  sig
+    type form_info =
+      SmtCnf.MakeCnf(Form).form_info =
+        Immediate of bool
+      | Done
+      | Todo
+    val info : (int, form_info) Hashtbl.t
+    val init_last : Form.t SmtCertif.clause
+    val last : Form.t SmtCertif.clause ref
+    val cnf_todo : Form.t array list ref
+    val clear : unit -> unit
+    val push_cnf : Form.t array -> unit
+    val get_info : Form.t -> form_info
+    val set_done : Form.t -> unit
+    val set_immediate : Form.t -> unit
+    val test_immediate : Form.t -> bool
+    val check_trivial : Form.t list -> bool
+    val link_Other : Form.t SmtCertif.rule -> Form.t list -> unit
+    val both_lit : Form.t -> Form.t * Form.t
+    val or_of_imp : Form.t array -> Form.t array
+    val cnf : Form.t -> unit
+    exception Cnf_done
+    val imm_link_Other : Form.t SmtCertif.rule -> Form.t -> unit
+    val imm_cnf : Form.t SmtCertif.clause -> unit
+    val make_cnf :
+      Form.reify -> Form.t SmtCertif.clause -> Form.t SmtCertif.clause
+  end
diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli
new file mode 100644
index 0000000..dee465c
--- /dev/null
+++ b/src/trace/smtCertif.mli
@@ -0,0 +1,42 @@
+type used = int
+type clause_id = int
+type 'hform rule =
+    ImmFlatten of 'hform clause * 'hform
+  | True
+  | False
+  | BuildDef of 'hform
+  | BuildDef2 of 'hform
+  | BuildProj of 'hform * int
+  | ImmBuildDef of 'hform clause
+  | ImmBuildDef2 of 'hform clause
+  | ImmBuildProj of 'hform clause * int
+  | EqTr of 'hform * 'hform list
+  | EqCgr of 'hform * 'hform option list
+  | EqCgrP of 'hform * 'hform * 'hform option list
+  | LiaMicromega of 'hform list *
+      Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+  | LiaDiseq of 'hform
+  | SplArith of 'hform clause * 'hform *
+      Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+  | SplDistinctElim of 'hform clause * 'hform
+  | Hole of 'hform clause list * 'hform list
+and 'hform clause = {
+  id : clause_id;
+  mutable kind : 'hform clause_kind;
+  mutable pos : int option;
+  mutable used : used;
+  mutable prev : 'hform clause option;
+  mutable next : 'hform clause option;
+  value : 'hform list option;
+}
+and 'hform clause_kind =
+    Root
+  | Same of 'hform clause
+  | Res of 'hform resolution
+  | Other of 'hform rule
+and 'hform resolution = {
+  mutable rc1 : 'hform clause;
+  mutable rc2 : 'hform clause;
+  mutable rtail : 'hform clause list;
+}
+val used_clauses : 'a rule -> 'a clause list
diff --git a/src/trace/smtCnf.mli b/src/trace/smtCnf.mli
new file mode 100644
index 0000000..47fbd8c
--- /dev/null
+++ b/src/trace/smtCnf.mli
@@ -0,0 +1,25 @@
+module MakeCnf :
+  functor (Form : SmtForm.FORM) ->
+    sig
+      type form_info = Immediate of bool | Done | Todo
+      val info : (int, form_info) Hashtbl.t
+      val init_last : Form.t SmtCertif.clause
+      val last : Form.t SmtCertif.clause ref
+      val cnf_todo : Form.t array list ref
+      val clear : unit -> unit
+      val push_cnf : Form.t array -> unit
+      val get_info : Form.t -> form_info
+      val set_done : Form.t -> unit
+      val set_immediate : Form.t -> unit
+      val test_immediate : Form.t -> bool
+      val check_trivial : Form.t list -> bool
+      val link_Other : Form.t SmtCertif.rule -> Form.t list -> unit
+      val both_lit : Form.t -> Form.t * Form.t
+      val or_of_imp : Form.t array -> Form.t array
+      val cnf : Form.t -> unit
+      exception Cnf_done
+      val imm_link_Other : Form.t SmtCertif.rule -> Form.t -> unit
+      val imm_cnf : Form.t SmtCertif.clause -> unit
+      val make_cnf :
+        Form.reify -> Form.t SmtCertif.clause -> Form.t SmtCertif.clause
+    end
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
new file mode 100644
index 0000000..b90e3ff
--- /dev/null
+++ b/src/trace/smtCommands.mli
@@ -0,0 +1,92 @@
+val euf_checker_modules : string list list
+val certif_ops :
+  Term.constr array option ->
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t
+val cCertif : Term.constr lazy_t
+val ccertif : Term.constr lazy_t
+val cchecker : Term.constr lazy_t
+val cchecker_correct : Term.constr lazy_t
+val cchecker_b_correct : Term.constr lazy_t
+val cchecker_b : Term.constr lazy_t
+val cchecker_eq_correct : Term.constr lazy_t
+val cchecker_eq : Term.constr lazy_t
+val compute_roots :
+  SmtAtom.Form.t list -> SmtAtom.Form.t SmtCertif.clause -> int list
+val interp_uf :
+  (int, Term.constr) Hashtbl.t ->
+  (int, Term.constr) Hashtbl.t -> SmtAtom.Form.t list -> Term.constr
+val interp_conseq_uf :
+  SmtAtom.Form.t list list * SmtAtom.Form.t list -> Term.types
+val print_assm : Term.constr -> unit
+val parse_certif :
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtAtom.Form.reify * SmtAtom.Form.t list * int *
+  SmtAtom.Form.t SmtCertif.clause -> unit
+val interp_roots : SmtAtom.Form.t list -> Term.constr
+val theorem :
+  Names.identifier ->
+  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtAtom.Form.reify * SmtAtom.Form.t list * int *
+  SmtAtom.Form.t SmtCertif.clause -> unit
+val checker :
+  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtAtom.Form.reify * SmtAtom.Form.t list * int *
+  SmtAtom.Form.t SmtCertif.clause -> unit
+val build_body :
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  Term.constr ->
+  Term.constr ->
+  int * SmtAtom.Form.t SmtCertif.clause ->
+  Term.constr * Term.constr * (Names.identifier * Term.types) list
+val build_body_eq :
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  Term.constr ->
+  Term.constr ->
+  Term.constr ->
+  int * SmtAtom.Form.t SmtCertif.clause ->
+  Term.constr * Term.constr * (Names.identifier * Term.types) list
+val get_arguments : Term.constr -> Term.constr * Term.constr
+val make_proof :
+  ('a ->
+   'b ->
+   SmtAtom.Form.t -> SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t -> 'c) ->
+  'a -> 'b -> SmtAtom.Form.reify -> SmtAtom.Form.t -> 'c
+val core_tactic :
+  (SmtAtom.Btype.reify_tbl ->
+   SmtAtom.Op.reify_tbl ->
+   SmtAtom.Form.t ->
+   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
+   int * SmtAtom.Form.t SmtCertif.clause) ->
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl ->
+  SmtAtom.Form.reify ->
+  Environ.env -> Evd.evar_map -> Term.constr -> Proof_type.tactic
+val tactic :
+  (SmtAtom.Btype.reify_tbl ->
+   SmtAtom.Op.reify_tbl ->
+   SmtAtom.Form.t ->
+   SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
+   int * SmtAtom.Form.t SmtCertif.clause) ->
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Atom.reify_tbl -> SmtAtom.Form.reify -> Proof_type.tactic
diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli
new file mode 100644
index 0000000..d6aa792
--- /dev/null
+++ b/src/trace/smtMisc.mli
@@ -0,0 +1,7 @@
+val cInt_tbl : (int, Term.constr) Hashtbl.t
+val mkInt : int -> Term.constr
+type 'a gen_hashed = { index : int; hval : 'a; }
+val mklApp : Term.constr Lazy.t -> Term.constr array -> Term.constr
+val declare_new_type : Names.variable -> Term.constr
+val declare_new_variable : Names.variable -> Term.types -> Term.constr
+val mkName : string -> Names.name
diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli
new file mode 100644
index 0000000..533725b
--- /dev/null
+++ b/src/trace/smtTrace.mli
@@ -0,0 +1,81 @@
+val notUsed : int
+val clear : unit -> unit
+val next_id : unit -> SmtCertif.clause_id
+val mk_scertif :
+  'a SmtCertif.clause_kind -> 'a list option -> 'a SmtCertif.clause
+val mkRootGen : 'a list option -> 'a SmtCertif.clause
+val mkRootV : 'a list -> 'a SmtCertif.clause
+val isRoot : 'a SmtCertif.clause_kind -> bool
+val mkRes :
+  'a SmtCertif.clause ->
+  'a SmtCertif.clause -> 'a SmtCertif.clause list -> 'a SmtCertif.clause
+val isRes : 'a SmtCertif.clause_kind -> bool
+val mkOther : 'a SmtCertif.rule -> 'a list option -> 'a SmtCertif.clause
+val next : 'a SmtCertif.clause -> 'a SmtCertif.clause
+val has_prev : 'a SmtCertif.clause -> bool
+val prev : 'a SmtCertif.clause -> 'a SmtCertif.clause
+val link : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit
+val clear_links : 'a SmtCertif.clause -> unit
+val skip : 'a SmtCertif.clause -> unit
+val insert_before : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit
+val get_res : 'a SmtCertif.clause -> string -> 'a SmtCertif.resolution
+val get_other : 'a SmtCertif.clause -> string -> 'a SmtCertif.rule
+val get_val : 'a SmtCertif.clause -> 'a list
+val repr : 'a SmtCertif.clause -> 'a SmtCertif.clause
+val set_same : 'a SmtCertif.clause -> 'a SmtCertif.clause -> unit
+val get_pos : 'a SmtCertif.clause -> int
+val eq_clause : 'a SmtCertif.clause -> 'b SmtCertif.clause -> bool
+val select : 'a SmtCertif.clause -> unit
+val occur : 'a SmtCertif.clause -> unit
+val alloc : 'a SmtCertif.clause -> int
+val naive_alloc : 'a SmtCertif.clause -> int
+val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int
+val to_coq :
+  ('a -> Term.constr) ->
+  ('a list list * 'a list -> 'b) ->
+  Term.types Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t * Term.constr Lazy.t * Term.constr Lazy.t *
+  Term.constr Lazy.t ->
+  'a SmtCertif.clause ->
+  Term.constr * 'a SmtCertif.clause * (Names.identifier * 'b) list
+module MakeOpt :
+  functor (Form : SmtForm.FORM) ->
+    sig
+      val share_value : Form.t SmtCertif.clause -> unit
+      module HashedHeadRes :
+        sig
+          type t = Form.t SmtCertif.resolution
+          val equal :
+            'a SmtCertif.resolution -> 'b SmtCertif.resolution -> bool
+          val hash : 'a SmtCertif.resolution -> int
+        end
+      module HRtbl :
+        sig
+          type key = HashedHeadRes.t
+          type 'a t = 'a Hashtbl.Make(HashedHeadRes).t
+          val create : int -> 'a t
+          val clear : 'a t -> unit
+          val reset : 'a t -> unit
+          val copy : 'a t -> 'a t
+          val add : 'a t -> key -> 'a -> unit
+          val remove : 'a t -> key -> unit
+          val find : 'a t -> key -> 'a
+          val find_all : 'a t -> key -> 'a list
+          val replace : 'a t -> key -> 'a -> unit
+          val mem : 'a t -> key -> bool
+          val iter : (key -> 'a -> unit) -> 'a t -> unit
+          val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
+          val length : 'a t -> int
+          val stats : 'a t -> Hashtbl.statistics
+        end
+      val common_head :
+        'a SmtCertif.clause list ->
+        'b SmtCertif.clause list ->
+        'a SmtCertif.clause list * 'a SmtCertif.clause list *
+        'b SmtCertif.clause list
+      val share_prefix : Form.t SmtCertif.clause -> int -> unit
+    end
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
new file mode 100644
index 0000000..2ec830c
--- /dev/null
+++ b/src/verit/verit.mli
@@ -0,0 +1,31 @@
+val debug : bool
+val import_trace :
+  string ->
+  (SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t) option ->
+  int * SmtAtom.Form.t SmtCertif.clause
+val clear_all : unit -> unit
+val import_all :
+  string ->
+  string ->
+  SmtAtom.Btype.reify_tbl * SmtAtom.Op.reify_tbl * SmtAtom.Atom.reify_tbl *
+  SmtAtom.Form.reify * SmtAtom.Form.t list * int *
+  SmtAtom.Form.t SmtCertif.clause
+val parse_certif :
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier ->
+  Names.identifier -> Names.identifier -> string -> string -> unit
+val theorem : Names.identifier -> string -> string -> unit
+val checker : string -> string -> unit
+val export :
+  out_channel ->
+  SmtAtom.Btype.reify_tbl -> SmtAtom.Op.reify_tbl -> SmtAtom.Form.t -> unit
+val call_verit :
+  SmtAtom.Btype.reify_tbl ->
+  SmtAtom.Op.reify_tbl ->
+  SmtAtom.Form.t ->
+  SmtAtom.Form.t SmtCertif.clause * SmtAtom.Form.t ->
+  int * SmtAtom.Form.t SmtCertif.clause
+val tactic : unit -> Proof_type.tactic
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
diff --git a/src/zchaff/cnfParser.mli b/src/zchaff/cnfParser.mli
new file mode 100644
index 0000000..4e2e079
--- /dev/null
+++ b/src/zchaff/cnfParser.mli
@@ -0,0 +1,13 @@
+val skip_comment : SatParser.lex_buff -> unit
+val parse_p_cnf : SatParser.lex_buff -> int
+val mklit : int -> SatAtom.Form.reify -> int -> SatAtom.Form.t
+val parse_clause :
+  int -> SatAtom.Form.reify -> SatParser.lex_buff -> SatAtom.Form.t list
+val parse_clauses :
+  int ->
+  SatAtom.Form.reify ->
+  SatParser.lex_buff ->
+  SatAtom.Form.t SmtCertif.clause -> SatAtom.Form.t SmtCertif.clause
+val parse_cnf :
+  string ->
+  int * SatAtom.Form.t SmtCertif.clause * SatAtom.Form.t SmtCertif.clause
diff --git a/src/zchaff/satParser.mli b/src/zchaff/satParser.mli
new file mode 100644
index 0000000..ad5385b
--- /dev/null
+++ b/src/zchaff/satParser.mli
@@ -0,0 +1,33 @@
+type lex_buff = {
+  buff : string;
+  mutable curr_char : int;
+  mutable buff_end : int;
+  in_ch : in_channel;
+}
+val buff_length : int
+val open_file : string -> string -> lex_buff
+val close : lex_buff -> unit
+val eof : lex_buff -> bool
+val curr_char : lex_buff -> char
+val refill : lex_buff -> unit
+val is_space : char -> bool
+val is_space_ret : char -> bool
+val skip : (char -> bool) -> lex_buff -> unit
+val skip_space : lex_buff -> unit
+val skip_blank : lex_buff -> unit
+val skip_string : lex_buff -> string -> bool
+val match_string : lex_buff -> string -> unit
+val aux_buff : bytes
+val aux_be : int ref
+val aux_pi : int ref
+val aux_cc : int ref
+val save_lb : lex_buff -> unit
+val restore_lb : lex_buff -> unit
+val check_string : lex_buff -> string -> bool
+val blank_check_string : lex_buff -> string -> bool
+val blank_match_string : lex_buff -> string -> unit
+val is_digit : char -> bool
+val is_start_int : lex_buff -> bool
+val input_int : lex_buff -> int
+val input_blank_int : lex_buff -> int
+val skip_line : lex_buff -> unit
diff --git a/src/zchaff/zchaff.mli b/src/zchaff/zchaff.mli
new file mode 100644
index 0000000..ff0fe51
--- /dev/null
+++ b/src/zchaff/zchaff.mli
@@ -0,0 +1,88 @@
+val is_trivial : SatAtom.Form.t list -> bool
+val string_of_op : SmtForm.fop -> string
+val pp_form : Format.formatter -> SatAtom.Form.t -> unit
+val pp_sign : Format.formatter -> SatAtom.Form.t -> unit
+val pp_pform : Format.formatter -> SatAtom.Form.pform -> unit
+val pp_value : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit
+val pp_kind : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit
+val pp_trace : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit
+val import_cnf :
+  string ->
+  int * SatAtom.Form.t SmtCertif.clause * SatAtom.Form.t SmtCertif.clause *
+  (int, SatAtom.Form.t SmtCertif.clause) Hashtbl.t
+val import_cnf_trace :
+  (int, 'a SmtCertif.clause) Hashtbl.t ->
+  string ->
+  SatAtom.Form.t SmtCertif.clause ->
+  'a SmtCertif.clause -> int * 'a SmtCertif.clause
+val make_roots :
+  SatAtom.Form.t SmtCertif.clause -> 'a SmtCertif.clause -> Term.constr
+val interp_roots :
+  SatAtom.Form.t SmtCertif.clause -> 'a SmtCertif.clause -> Term.constr
+val sat_checker_modules : string list list
+val parse_certif :
+  Names.identifier -> Names.identifier -> string -> string -> unit
+val cdimacs : Term.constr lazy_t
+val ctheorem_checker : Term.constr lazy_t
+val cchecker : Term.constr lazy_t
+val theorems :
+  (Term.constr ->
+   SatAtom.Form.t SmtCertif.clause ->
+   SatAtom.Form.t SmtCertif.clause -> Term.constr) ->
+  Names.identifier -> string -> string -> unit
+val theorem : Names.identifier -> string -> string -> unit
+val theorem_abs : Names.identifier -> string -> string -> unit
+val checker : string -> string -> unit
+val export_clause : Format.formatter -> SatAtom.Form.t list -> unit
+val export :
+  out_channel ->
+  int ->
+  SatAtom.Form.t SmtCertif.clause ->
+  (int, SatAtom.Form.t SmtCertif.clause) Hashtbl.t *
+  SatAtom.Form.t SmtCertif.clause
+val call_zchaff :
+  int ->
+  SatAtom.Form.t SmtCertif.clause ->
+  (int, SatAtom.Form.t SmtCertif.clause) Hashtbl.t * string * string *
+  SatAtom.Form.t SmtCertif.clause
+val cnf_checker_modules : string list list
+val certif_ops :
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t * Term.constr lazy_t * Term.constr lazy_t *
+  Term.constr lazy_t
+val ccertif : Term.constr lazy_t
+val cCertif : Term.constr lazy_t
+val cchecker_b_correct : Term.constr lazy_t
+val cchecker_b : Term.constr lazy_t
+val cchecker_eq_correct : Term.constr lazy_t
+val cchecker_eq : Term.constr lazy_t
+val build_body :
+  SatAtom.Atom.reify_tbl ->
+  SatAtom.Form.reify ->
+  Term.constr ->
+  Term.constr ->
+  int * SatAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr
+val build_body_eq :
+  SatAtom.Atom.reify_tbl ->
+  SatAtom.Form.reify ->
+  Term.constr ->
+  Term.constr ->
+  Term.constr ->
+  int * SatAtom.Form.t SmtCertif.clause -> Term.constr * Term.constr
+val get_arguments : Term.constr -> Term.constr * Term.constr
+exception Sat of int list
+exception Finished
+val input_int : in_channel -> int
+val check_unsat : string -> unit
+val make_proof :
+  (int, 'a) SmtForm.gen_pform array ->
+  Term.constr array ->
+  Environ.env ->
+  SatAtom.Form.reify ->
+  SatAtom.Form.t -> int * SatAtom.Form.t SmtCertif.clause
+val core_tactic : Environ.env -> 'a -> Term.types -> Proof_type.tactic
+val tactic : unit -> Proof_type.tactic
diff --git a/src/zchaff/zchaffParser.mli b/src/zchaff/zchaffParser.mli
new file mode 100644
index 0000000..a512f48
--- /dev/null
+++ b/src/zchaff/zchaffParser.mli
@@ -0,0 +1,36 @@
+val _CL : string
+val _INF : string
+val _VAR : string
+val _L : string
+val _V : string
+val _A : string
+val _LITS : string
+val _CONF : string
+val _EQ : string
+val alloc_res :
+  'a SmtCertif.clause ->
+  'a SmtCertif.clause ->
+  'a SmtCertif.clause -> 'a SmtCertif.clause list -> 'a SmtCertif.clause
+val parse_tailres : (int, 'a) Hashtbl.t -> SatParser.lex_buff -> 'a list
+val parse_resolution :
+  (int, 'a SmtCertif.clause) Hashtbl.t ->
+  SatParser.lex_buff -> 'a SmtCertif.clause -> 'a SmtCertif.clause
+val parse_CL :
+  (int, 'a SmtCertif.clause) Hashtbl.t ->
+  SatParser.lex_buff -> 'a SmtCertif.clause -> 'a SmtCertif.clause
+type var_key = Var of int | Level of int
+type 'hform var_decl = {
+  var : int;
+  ante : 'hform SmtCertif.clause;
+  ante_val : int list;
+  mutable vclause : 'hform SmtCertif.clause option;
+}
+type 'hform parse_var_info = (var_key, 'hform var_decl) Hashtbl.t
+val var_of_lit : int -> int
+val parse_zclause : SatParser.lex_buff -> int list
+val parse_VAR_CONF :
+  (int, 'a SmtCertif.clause) Hashtbl.t ->
+  SatParser.lex_buff -> 'a SmtCertif.clause -> 'a SmtCertif.clause
+val parse_proof :
+  (int, 'a SmtCertif.clause) Hashtbl.t ->
+  string -> 'a SmtCertif.clause -> 'a SmtCertif.clause