Merge remote-tracking branch 'origin/coq-8.12' into coq-8.13

19 files changed, 983 insertions, 585 deletions

diff --git a/src/Misc.v b/src/Misc.v
index e558ce3..5590e14 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -1420,6 +1420,29 @@ Lemma is_true_iff e :  e = true <-> is_true e.
 Proof. now unfold is_true. Qed.
 
 
+(* Register constants for OCaml access *)
+Register distinct as SMTCoq.Misc.distinct.
+
+Register Int63.eqb as num.int63.eqb.
+Register PArray.array as array.array.type.
+Register PArray.make as array.array.make.
+Register PArray.set as array.array.set.
+Register Coq.Init.Datatypes.is_true as core.is_true.is_true.
+Register Coq.PArith.BinPosDef.Pos.eqb as num.pos.eqb.
+Register Coq.NArith.BinNat.N.of_nat as num.N.of_nat.
+Register Coq.ZArith.BinInt.Z.ltb as num.Z.ltb.
+Register Coq.ZArith.BinInt.Z.leb as num.Z.leb.
+Register Coq.ZArith.BinInt.Z.gtb as num.Z.gtb.
+Register Coq.ZArith.BinInt.Z.geb as num.Z.geb.
+Register Coq.ZArith.BinInt.Z.eqb as num.Z.eqb.
+Register Coq.Init.Datatypes.implb as core.bool.implb.
+Register Coq.Bool.Bool.eqb as core.bool.eqb.
+Register Coq.Bool.Bool.ifb as core.bool.ifb.
+Register Coq.Bool.Bool.reflect as core.bool.reflect.
+Register Coq.Init.Datatypes.length as core.list.length.
+Register Coq.micromega.ZMicromega.ZArithProof as micromega.ZMicromega.ZArithProof.
+
+
 (* 
    Local Variables:
    coq-load-path: ((rec "." "SMTCoq"))
diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index 56ac458..c0d109f 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -2608,6 +2608,79 @@ End PredefinedArrays.
 *)
 
 
+(* Register constants for OCaml access *)
+Register Typ.type as SMTCoq.SMT_terms.Typ.type.
+Register Typ.TFArray as SMTCoq.SMT_terms.Typ.TFArray.
+Register Typ.Tindex as SMTCoq.SMT_terms.Typ.Tindex.
+Register Typ.TZ as SMTCoq.SMT_terms.Typ.TZ.
+Register Typ.Tbool as SMTCoq.SMT_terms.Typ.Tbool.
+Register Typ.Tpositive as SMTCoq.SMT_terms.Typ.Tpositive.
+Register Typ.TBV as SMTCoq.SMT_terms.Typ.TBV.
+Register Typ.interp as SMTCoq.SMT_terms.Typ.interp.
+Register Typ.dec_interp as SMTCoq.SMT_terms.Typ.dec_interp.
+Register Typ.ord_interp as SMTCoq.SMT_terms.Typ.ord_interp.
+Register Typ.comp_interp as SMTCoq.SMT_terms.Typ.comp_interp.
+Register Typ.inh_interp as SMTCoq.SMT_terms.Typ.inh_interp.
+Register Typ.i_eqb as SMTCoq.SMT_terms.Typ.i_eqb.
+Register Atom.tval as SMTCoq.SMT_terms.Atom.tval.
+Register Atom.Tval as SMTCoq.SMT_terms.Atom.Tval.
+Register Atom.CO_xH as SMTCoq.SMT_terms.Atom.CO_xH.
+Register Atom.CO_Z0 as SMTCoq.SMT_terms.Atom.CO_Z0.
+Register Atom.CO_BV as SMTCoq.SMT_terms.Atom.CO_BV.
+Register Atom.UO_xO as SMTCoq.SMT_terms.Atom.UO_xO.
+Register Atom.UO_xI as SMTCoq.SMT_terms.Atom.UO_xI.
+Register Atom.UO_Zpos as SMTCoq.SMT_terms.Atom.UO_Zpos.
+Register Atom.UO_Zneg as SMTCoq.SMT_terms.Atom.UO_Zneg.
+Register Atom.UO_Zopp as SMTCoq.SMT_terms.Atom.UO_Zopp.
+Register Atom.UO_BVbitOf as SMTCoq.SMT_terms.Atom.UO_BVbitOf.
+Register Atom.UO_BVnot as SMTCoq.SMT_terms.Atom.UO_BVnot.
+Register Atom.UO_BVneg as SMTCoq.SMT_terms.Atom.UO_BVneg.
+Register Atom.UO_BVextr as SMTCoq.SMT_terms.Atom.UO_BVextr.
+Register Atom.UO_BVzextn as SMTCoq.SMT_terms.Atom.UO_BVzextn.
+Register Atom.UO_BVsextn as SMTCoq.SMT_terms.Atom.UO_BVsextn.
+Register Atom.BO_Zplus as SMTCoq.SMT_terms.Atom.BO_Zplus.
+Register Atom.BO_Zminus as SMTCoq.SMT_terms.Atom.BO_Zminus.
+Register Atom.BO_Zmult as SMTCoq.SMT_terms.Atom.BO_Zmult.
+Register Atom.BO_Zlt as SMTCoq.SMT_terms.Atom.BO_Zlt.
+Register Atom.BO_Zle as SMTCoq.SMT_terms.Atom.BO_Zle.
+Register Atom.BO_Zge as SMTCoq.SMT_terms.Atom.BO_Zge.
+Register Atom.BO_Zgt as SMTCoq.SMT_terms.Atom.BO_Zgt.
+Register Atom.BO_eq as SMTCoq.SMT_terms.Atom.BO_eq.
+Register Atom.BO_BVand as SMTCoq.SMT_terms.Atom.BO_BVand.
+Register Atom.BO_BVor as SMTCoq.SMT_terms.Atom.BO_BVor.
+Register Atom.BO_BVxor as SMTCoq.SMT_terms.Atom.BO_BVxor.
+Register Atom.BO_BVadd as SMTCoq.SMT_terms.Atom.BO_BVadd.
+Register Atom.BO_BVmult as SMTCoq.SMT_terms.Atom.BO_BVmult.
+Register Atom.BO_BVult as SMTCoq.SMT_terms.Atom.BO_BVult.
+Register Atom.BO_BVslt as SMTCoq.SMT_terms.Atom.BO_BVslt.
+Register Atom.BO_BVconcat as SMTCoq.SMT_terms.Atom.BO_BVconcat.
+Register Atom.BO_BVshl as SMTCoq.SMT_terms.Atom.BO_BVshl.
+Register Atom.BO_BVshr as SMTCoq.SMT_terms.Atom.BO_BVshr.
+Register Atom.BO_select as SMTCoq.SMT_terms.Atom.BO_select.
+Register Atom.BO_diffarray as SMTCoq.SMT_terms.Atom.BO_diffarray.
+Register Atom.TO_store as SMTCoq.SMT_terms.Atom.TO_store.
+Register Atom.NO_distinct as SMTCoq.SMT_terms.Atom.NO_distinct.
+Register Atom.atom as SMTCoq.SMT_terms.Atom.atom.
+Register Atom.Acop as SMTCoq.SMT_terms.Atom.Acop.
+Register Atom.Auop as SMTCoq.SMT_terms.Atom.Auop.
+Register Atom.Abop as SMTCoq.SMT_terms.Atom.Abop.
+Register Atom.Atop as SMTCoq.SMT_terms.Atom.Atop.
+Register Atom.Anop as SMTCoq.SMT_terms.Atom.Anop.
+Register Atom.Aapp as SMTCoq.SMT_terms.Atom.Aapp.
+Register Form.form as SMTCoq.SMT_terms.Form.form.
+Register Form.Fatom as SMTCoq.SMT_terms.Form.Fatom.
+Register Form.Ftrue as SMTCoq.SMT_terms.Form.Ftrue.
+Register Form.Ffalse as SMTCoq.SMT_terms.Form.Ffalse.
+Register Form.Fnot2 as SMTCoq.SMT_terms.Form.Fnot2.
+Register Form.Fand as SMTCoq.SMT_terms.Form.Fand.
+Register Form.For as SMTCoq.SMT_terms.Form.For.
+Register Form.Fxor as SMTCoq.SMT_terms.Form.Fxor.
+Register Form.Fimp as SMTCoq.SMT_terms.Form.Fimp.
+Register Form.Fiff as SMTCoq.SMT_terms.Form.Fiff.
+Register Form.Fite as SMTCoq.SMT_terms.Form.Fite.
+Register Form.FbbT as SMTCoq.SMT_terms.Form.FbbT.
+
+
 (* 
    Local Variables:
    coq-load-path: ((rec "." "SMTCoq"))
diff --git a/src/State.v b/src/State.v
index ae69f37..1f295ce 100644
--- a/src/State.v
+++ b/src/State.v
@@ -737,3 +737,8 @@ Module S.
 
   
 End S.
+
+
+(* Register constants for OCaml access *)
+Register C.t as SMTCoq.State.C.t.
+Register S.t as SMTCoq.State.S.t.
diff --git a/src/Trace.v b/src/Trace.v
index 3f61dc7..85671f9 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -778,6 +778,127 @@ End Euf_Checker.
 Unset Implicit Arguments.
 
 
+(* Register constants for OCaml access *)
+Register Sat_Checker.valid as SMTCoq.Trace.Sat_Checker.valid.
+Register Sat_Checker.interp_var as SMTCoq.Trace.Sat_Checker.interp_var.
+Register Sat_Checker.Certif as SMTCoq.Trace.Sat_Checker.Certif.
+Register Sat_Checker.step as SMTCoq.Trace.Sat_Checker.step.
+Register Sat_Checker.Res as SMTCoq.Trace.Sat_Checker.Res.
+Register Sat_Checker.dimacs as SMTCoq.Trace.Sat_Checker.dimacs.
+Register Sat_Checker.certif as SMTCoq.Trace.Sat_Checker.certif.
+Register Sat_Checker.theorem_checker as SMTCoq.Trace.Sat_Checker.theorem_checker.
+Register Sat_Checker.checker as SMTCoq.Trace.Sat_Checker.checker.
+
+Register Cnf_Checker.certif as SMTCoq.Trace.Cnf_Checker.certif.
+Register Cnf_Checker.Certif as SMTCoq.Trace.Cnf_Checker.Certif.
+Register Cnf_Checker.checker_b_correct as SMTCoq.Trace.Cnf_Checker.checker_b_correct.
+Register Cnf_Checker.checker_b as SMTCoq.Trace.Cnf_Checker.checker_b.
+Register Cnf_Checker.checker_eq_correct as SMTCoq.Trace.Cnf_Checker.checker_eq_correct.
+Register Cnf_Checker.checker_eq as SMTCoq.Trace.Cnf_Checker.checker_eq.
+Register Cnf_Checker.step as SMTCoq.Trace.Cnf_Checker.step.
+Register Cnf_Checker.Res as SMTCoq.Trace.Cnf_Checker.Res.
+Register Cnf_Checker.ImmFlatten as SMTCoq.Trace.Cnf_Checker.ImmFlatten.
+Register Cnf_Checker.CTrue as SMTCoq.Trace.Cnf_Checker.CTrue.
+Register Cnf_Checker.CFalse as SMTCoq.Trace.Cnf_Checker.CFalse.
+Register Cnf_Checker.BuildDef as SMTCoq.Trace.Cnf_Checker.BuildDef.
+Register Cnf_Checker.BuildDef2 as SMTCoq.Trace.Cnf_Checker.BuildDef2.
+Register Cnf_Checker.BuildProj as SMTCoq.Trace.Cnf_Checker.BuildProj.
+Register Cnf_Checker.ImmBuildDef as SMTCoq.Trace.Cnf_Checker.ImmBuildDef.
+Register Cnf_Checker.ImmBuildDef2 as SMTCoq.Trace.Cnf_Checker.ImmBuildDef2.
+Register Cnf_Checker.ImmBuildProj as SMTCoq.Trace.Cnf_Checker.ImmBuildProj.
+
+Register Euf_Checker.Certif as SMTCoq.Trace.Euf_Checker.Certif.
+Register Euf_Checker.certif as SMTCoq.Trace.Euf_Checker.certif.
+Register Euf_Checker.checker as SMTCoq.Trace.Euf_Checker.checker.
+Register Euf_Checker.checker_correct as SMTCoq.Trace.Euf_Checker.checker_correct.
+Register Euf_Checker.checker_b_correct as SMTCoq.Trace.Euf_Checker.checker_b_correct.
+Register Euf_Checker.checker_b as SMTCoq.Trace.Euf_Checker.checker_b.
+Register Euf_Checker.checker_eq_correct as SMTCoq.Trace.Euf_Checker.checker_eq_correct.
+Register Euf_Checker.checker_eq as SMTCoq.Trace.Euf_Checker.checker_eq.
+Register Euf_Checker.checker_debug as SMTCoq.Trace.Euf_Checker.checker_debug.
+Register Euf_Checker.name_step as SMTCoq.Trace.Euf_Checker.name_step.
+Register Euf_Checker.Name_Res as SMTCoq.Trace.Euf_Checker.Name_Res.
+Register Euf_Checker.Name_Weaken as SMTCoq.Trace.Euf_Checker.Name_Weaken.
+Register Euf_Checker.Name_ImmFlatten as SMTCoq.Trace.Euf_Checker.Name_ImmFlatten.
+Register Euf_Checker.Name_CTrue as SMTCoq.Trace.Euf_Checker.Name_CTrue.
+Register Euf_Checker.Name_CFalse as SMTCoq.Trace.Euf_Checker.Name_CFalse.
+Register Euf_Checker.Name_BuildDef as SMTCoq.Trace.Euf_Checker.Name_BuildDef.
+Register Euf_Checker.Name_BuildDef2 as SMTCoq.Trace.Euf_Checker.Name_BuildDef2.
+Register Euf_Checker.Name_BuildProj as SMTCoq.Trace.Euf_Checker.Name_BuildProj.
+Register Euf_Checker.Name_ImmBuildDef as SMTCoq.Trace.Euf_Checker.Name_ImmBuildDef.
+Register Euf_Checker.Name_ImmBuildDef2 as SMTCoq.Trace.Euf_Checker.Name_ImmBuildDef2.
+Register Euf_Checker.Name_ImmBuildProj as SMTCoq.Trace.Euf_Checker.Name_ImmBuildProj.
+Register Euf_Checker.Name_EqTr as SMTCoq.Trace.Euf_Checker.Name_EqTr.
+Register Euf_Checker.Name_EqCgr as SMTCoq.Trace.Euf_Checker.Name_EqCgr.
+Register Euf_Checker.Name_EqCgrP as SMTCoq.Trace.Euf_Checker.Name_EqCgrP.
+Register Euf_Checker.Name_LiaMicromega as SMTCoq.Trace.Euf_Checker.Name_LiaMicromega.
+Register Euf_Checker.Name_LiaDiseq as SMTCoq.Trace.Euf_Checker.Name_LiaDiseq.
+Register Euf_Checker.Name_SplArith as SMTCoq.Trace.Euf_Checker.Name_SplArith.
+Register Euf_Checker.Name_SplDistinctElim as SMTCoq.Trace.Euf_Checker.Name_SplDistinctElim.
+Register Euf_Checker.Name_BBVar as SMTCoq.Trace.Euf_Checker.Name_BBVar.
+Register Euf_Checker.Name_BBConst as SMTCoq.Trace.Euf_Checker.Name_BBConst.
+Register Euf_Checker.Name_BBOp as SMTCoq.Trace.Euf_Checker.Name_BBOp.
+Register Euf_Checker.Name_BBNot as SMTCoq.Trace.Euf_Checker.Name_BBNot.
+Register Euf_Checker.Name_BBNeg as SMTCoq.Trace.Euf_Checker.Name_BBNeg.
+Register Euf_Checker.Name_BBAdd as SMTCoq.Trace.Euf_Checker.Name_BBAdd.
+Register Euf_Checker.Name_BBConcat as SMTCoq.Trace.Euf_Checker.Name_BBConcat.
+Register Euf_Checker.Name_BBMul as SMTCoq.Trace.Euf_Checker.Name_BBMul.
+Register Euf_Checker.Name_BBUlt as SMTCoq.Trace.Euf_Checker.Name_BBUlt.
+Register Euf_Checker.Name_BBSlt as SMTCoq.Trace.Euf_Checker.Name_BBSlt.
+Register Euf_Checker.Name_BBEq as SMTCoq.Trace.Euf_Checker.Name_BBEq.
+Register Euf_Checker.Name_BBDiseq as SMTCoq.Trace.Euf_Checker.Name_BBDiseq.
+Register Euf_Checker.Name_BBExtract as SMTCoq.Trace.Euf_Checker.Name_BBExtract.
+Register Euf_Checker.Name_BBZextend as SMTCoq.Trace.Euf_Checker.Name_BBZextend.
+Register Euf_Checker.Name_BBSextend as SMTCoq.Trace.Euf_Checker.Name_BBSextend.
+Register Euf_Checker.Name_BBShl as SMTCoq.Trace.Euf_Checker.Name_BBShl.
+Register Euf_Checker.Name_BBShr as SMTCoq.Trace.Euf_Checker.Name_BBShr.
+Register Euf_Checker.Name_RowEq as SMTCoq.Trace.Euf_Checker.Name_RowEq.
+Register Euf_Checker.Name_RowNeq as SMTCoq.Trace.Euf_Checker.Name_RowNeq.
+Register Euf_Checker.Name_Ext as SMTCoq.Trace.Euf_Checker.Name_Ext.
+Register Euf_Checker.Name_Hole as SMTCoq.Trace.Euf_Checker.Name_Hole.
+Register Euf_Checker.step as SMTCoq.Trace.Euf_Checker.step.
+Register Euf_Checker.Res as SMTCoq.Trace.Euf_Checker.Res.
+Register Euf_Checker.Weaken as SMTCoq.Trace.Euf_Checker.Weaken.
+Register Euf_Checker.ImmFlatten as SMTCoq.Trace.Euf_Checker.ImmFlatten.
+Register Euf_Checker.CTrue as SMTCoq.Trace.Euf_Checker.CTrue.
+Register Euf_Checker.CFalse as SMTCoq.Trace.Euf_Checker.CFalse.
+Register Euf_Checker.BuildDef as SMTCoq.Trace.Euf_Checker.BuildDef.
+Register Euf_Checker.BuildDef2 as SMTCoq.Trace.Euf_Checker.BuildDef2.
+Register Euf_Checker.BuildProj as SMTCoq.Trace.Euf_Checker.BuildProj.
+Register Euf_Checker.ImmBuildProj as SMTCoq.Trace.Euf_Checker.ImmBuildProj.
+Register Euf_Checker.ImmBuildDef as SMTCoq.Trace.Euf_Checker.ImmBuildDef.
+Register Euf_Checker.ImmBuildDef2 as SMTCoq.Trace.Euf_Checker.ImmBuildDef2.
+Register Euf_Checker.EqTr as SMTCoq.Trace.Euf_Checker.EqTr.
+Register Euf_Checker.EqCgr as SMTCoq.Trace.Euf_Checker.EqCgr.
+Register Euf_Checker.EqCgrP as SMTCoq.Trace.Euf_Checker.EqCgrP.
+Register Euf_Checker.LiaMicromega as SMTCoq.Trace.Euf_Checker.LiaMicromega.
+Register Euf_Checker.LiaDiseq as SMTCoq.Trace.Euf_Checker.LiaDiseq.
+Register Euf_Checker.SplArith as SMTCoq.Trace.Euf_Checker.SplArith.
+Register Euf_Checker.SplDistinctElim as SMTCoq.Trace.Euf_Checker.SplDistinctElim.
+Register Euf_Checker.BBVar as SMTCoq.Trace.Euf_Checker.BBVar.
+Register Euf_Checker.BBConst as SMTCoq.Trace.Euf_Checker.BBConst.
+Register Euf_Checker.BBOp as SMTCoq.Trace.Euf_Checker.BBOp.
+Register Euf_Checker.BBNot as SMTCoq.Trace.Euf_Checker.BBNot.
+Register Euf_Checker.BBEq as SMTCoq.Trace.Euf_Checker.BBEq.
+Register Euf_Checker.BBDiseq as SMTCoq.Trace.Euf_Checker.BBDiseq.
+Register Euf_Checker.BBNeg as SMTCoq.Trace.Euf_Checker.BBNeg.
+Register Euf_Checker.BBAdd as SMTCoq.Trace.Euf_Checker.BBAdd.
+Register Euf_Checker.BBMul as SMTCoq.Trace.Euf_Checker.BBMul.
+Register Euf_Checker.BBUlt as SMTCoq.Trace.Euf_Checker.BBUlt.
+Register Euf_Checker.BBSlt as SMTCoq.Trace.Euf_Checker.BBSlt.
+Register Euf_Checker.BBConcat as SMTCoq.Trace.Euf_Checker.BBConcat.
+Register Euf_Checker.BBExtract as SMTCoq.Trace.Euf_Checker.BBExtract.
+Register Euf_Checker.BBZextend as SMTCoq.Trace.Euf_Checker.BBZextend.
+Register Euf_Checker.BBSextend as SMTCoq.Trace.Euf_Checker.BBSextend.
+Register Euf_Checker.BBShl as SMTCoq.Trace.Euf_Checker.BBShl.
+Register Euf_Checker.BBShr as SMTCoq.Trace.Euf_Checker.BBShr.
+Register Euf_Checker.RowEq as SMTCoq.Trace.Euf_Checker.RowEq.
+Register Euf_Checker.RowNeq as SMTCoq.Trace.Euf_Checker.RowNeq.
+Register Euf_Checker.Ext as SMTCoq.Trace.Euf_Checker.Ext.
+Register Euf_Checker.Hole as SMTCoq.Trace.Euf_Checker.Hole.
+Register Euf_Checker.ForallInst as SMTCoq.Trace.Euf_Checker.ForallInst.
+
+
 (*
    Local Variables:
    coq-load-path: ((rec "." "SMTCoq"))
diff --git a/src/array/FArray.v b/src/array/FArray.v
index e45abb4..f46dcb7 100644
--- a/src/array/FArray.v
+++ b/src/array/FArray.v
@@ -1861,6 +1861,14 @@ Notation "a '[' i '<-' v ']'" := (store a i v)
    (at level 1, format "a [ i  <-  v ]") : farray_scope.
 
 
+(* Register constants for OCaml access *)
+Register FArray.farray as SMTCoq.array.FArray.farray.
+Register select as SMTCoq.array.FArray.select.
+Register store as SMTCoq.array.FArray.store.
+Register diff as SMTCoq.array.FArray.diff.
+Register FArray.equal as SMTCoq.array.FArray.equal.
+
+
 
 (* 
    Local Variables:
diff --git a/src/bva/BVList.v b/src/bva/BVList.v
index 5c707f6..b5a44e3 100644
--- a/src/bva/BVList.v
+++ b/src/bva/BVList.v
@@ -2541,6 +2541,29 @@ Module BITVECTOR_LIST <: BITVECTOR.
 
 End BITVECTOR_LIST.
 
+
+(* Register constants for OCaml access *)
+Register BITVECTOR_LIST.bitvector as SMTCoq.bva.BVList.BITVECTOR_LIST.bitvector.
+Register BITVECTOR_LIST.of_bits as SMTCoq.bva.BVList.BITVECTOR_LIST.of_bits.
+Register BITVECTOR_LIST.bitOf as SMTCoq.bva.BVList.BITVECTOR_LIST.bitOf.
+Register BITVECTOR_LIST.bv_eq as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_eq.
+Register BITVECTOR_LIST.bv_not as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_not.
+Register BITVECTOR_LIST.bv_neg as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_neg.
+Register BITVECTOR_LIST.bv_and as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_and.
+Register BITVECTOR_LIST.bv_or as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_or.
+Register BITVECTOR_LIST.bv_xor as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_xor.
+Register BITVECTOR_LIST.bv_add as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_add.
+Register BITVECTOR_LIST.bv_mult as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_mult.
+Register BITVECTOR_LIST.bv_ult as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_ult.
+Register BITVECTOR_LIST.bv_slt as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_slt.
+Register BITVECTOR_LIST.bv_concat as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_concat.
+Register BITVECTOR_LIST.bv_extr as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_extr.
+Register BITVECTOR_LIST.bv_zextn as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_zextn.
+Register BITVECTOR_LIST.bv_sextn as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_sextn.
+Register BITVECTOR_LIST.bv_shl as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_shl.
+Register BITVECTOR_LIST.bv_shr as SMTCoq.bva.BVList.BITVECTOR_LIST.bv_shr.
+
+
 (* 
    Local Variables:
    coq-load-path: ((rec ".." "SMTCoq"))
diff --git a/src/classes/SMT_classes.v b/src/classes/SMT_classes.v
index 1c050c9..9a33271 100644
--- a/src/classes/SMT_classes.v
+++ b/src/classes/SMT_classes.v
@@ -217,3 +217,12 @@ Section CompDec_from.
     Typ_compdec T CompDec_from.
 
 End CompDec_from.
+
+
+(* Register constants for OCaml access *)
+Register typ_compdec as SMTCoq.classes.SMT_classes.typ_compdec.
+Register Typ_compdec as SMTCoq.classes.SMT_classes.Typ_compdec.
+Register te_carrier as SMTCoq.classes.SMT_classes.te_carrier.
+Register te_compdec as SMTCoq.classes.SMT_classes.te_compdec.
+Register eqb_of_compdec as SMTCoq.classes.SMT_classes.eqb_of_compdec.
+Register CompDec as SMTCoq.classes.SMT_classes.CompDec.
diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index 1c8b2f6..0e51366 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -747,3 +747,12 @@ Section prod.
   |}.
 
 End prod.
+
+
+(* Register constants for OCaml access *)
+Register unit_typ_compdec as SMTCoq.classes.SMT_classes_instances.unit_typ_compdec.
+Register bool_compdec as SMTCoq.classes.SMT_classes_instances.bool_compdec.
+Register Z_compdec as SMTCoq.classes.SMT_classes_instances.Z_compdec.
+Register Positive_compdec as SMTCoq.classes.SMT_classes_instances.Positive_compdec.
+Register BV_compdec as SMTCoq.classes.SMT_classes_instances.BV_compdec.
+Register FArray_compdec as SMTCoq.classes.SMT_classes_instances.FArray_compdec.
diff --git a/src/trace/coqInterface.ml b/src/trace/coqInterface.ml
index f11563c..a3dc327 100644
--- a/src/trace/coqInterface.ml
+++ b/src/trace/coqInterface.ml
@@ -92,41 +92,13 @@ type econstr = EConstr.t
 let econstr_of_constr = EConstr.of_constr
 
 
-(* Modules *)
-let gen_constant_in_modules s m n =
-  (* UnivGen.constr_of_monomorphic_global will crash on universe polymorphic constants *)
-  UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules s m n
-let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
-let init_modules = Coqlib.init_modules
-
-
 (* Int63 *)
-let int63_module = [["Coq";"Numbers";"Cyclic";"Int63";"Int63"]]
-
 let mkInt : int -> Constr.constr =
   fun i -> Constr.mkInt (Uint63.of_int i)
 
-let cint = gen_constant int63_module "int"
-
 
 (* PArray *)
-let parray_modules = [["SMTCoq";"PArray";"PArray"]]
-
-let cmake = gen_constant parray_modules "make"
-let cset = gen_constant parray_modules "set"
-
 let max_array_size : int = 4194302
-let mkArray : Constr.types * Constr.t array -> Constr.t =
-  fun (ty, a) ->
-  let l = (Array.length a) - 1 in
-  snd (Array.fold_left (fun (i,acc) c ->
-                        let acc' =
-                          if i = l then
-                            acc
-                          else
-                            mkApp (Lazy.force cset, [|ty; acc; mkInt i; c|]) in
-                        (i+1,acc')
-                       ) (0, mkApp (Lazy.force cmake, [|ty; mkInt l; a.(l)|])) a)
 
 
 (* Traces *)
@@ -147,10 +119,6 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r =
 module Micromega_plugin_Micromega = Micromega_plugin.Micromega
 module Micromega_plugin_Certificate = Micromega_plugin.Certificate
 
-let micromega_coq_proofTerm =
-  (* Cannot contain evars *)
-  lazy (gen_constant_in_modules "ZMicromega" [["Coq"; "micromega";"ZMicromega"]] "ZArithProof")
-
 let micromega_dump_proof_term p =
   (* Cannot contain evars *)
   EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p)
diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli
index f450f6d..3352120 100644
--- a/src/trace/coqInterface.mli
+++ b/src/trace/coqInterface.mli
@@ -59,21 +59,12 @@ type econstr = EConstr.t
 val econstr_of_constr : constr -> econstr
 
 
-(* Modules *)
-val gen_constant : string list list -> string -> constr lazy_t
-val init_modules : string list list
-
-
 (* Int63 *)
-val int63_module : string list list
 val mkInt : int -> constr
-val cint : constr lazy_t
 
 
 (* PArray *)
-val parray_modules : string list list
 val max_array_size : int
-val mkArray : types * constr array -> constr
 
 
 (* Traces *)
@@ -91,8 +82,6 @@ val mkTrace :
 (* Micromega *)
 module Micromega_plugin_Micromega = Micromega_plugin.Micromega
 module Micromega_plugin_Certificate = Micromega_plugin.Certificate
-
-val micromega_coq_proofTerm : constr lazy_t
 val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr
 
 
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 67392bb..1dc5af0 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -13,276 +13,371 @@
 open SmtMisc
 
 
-let gen_constant = CoqInterface.gen_constant
+type coqTerm = CoqInterface.constr lazy_t
+
+let gc prefix constant =
+  lazy (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref (prefix ^ "." ^ constant)))
 
 
 (* Int63 *)
-let cint = CoqInterface.cint
-let ceq63 = gen_constant CoqInterface.int63_module "eqb"
+let int63_prefix = "num.int63"
+let int63_gc = gc int63_prefix
+let cint = int63_gc "type"
+let ceq63 = int63_gc "eqb"
 
 (* PArray *)
-let carray = gen_constant CoqInterface.parray_modules "array"
+let array_prefix = "array.array"
+let array_gc = gc array_prefix
+let carray = array_gc "type"
+let cmake = array_gc "make"
+let cset = array_gc "set"
 
 (* is_true *)
-let cis_true = gen_constant CoqInterface.init_modules "is_true"
+let cis_true = gc "core.is_true" "is_true"
 
 (* nat *)
-let cnat = gen_constant CoqInterface.init_modules "nat"
-let cO = gen_constant CoqInterface.init_modules "O"
-let cS = gen_constant CoqInterface.init_modules "S"
+let nat_prefix = "num.nat"
+let nat_gc = gc nat_prefix
+let cnat = nat_gc "type"
+let cO = nat_gc "O"
+let cS = nat_gc "S"
 
 (* Positive *)
-let positive_modules = [["Coq";"Numbers";"BinNums"];
-                        ["Coq";"PArith";"BinPosDef";"Pos"]]
-
-let cpositive = gen_constant positive_modules "positive"
-let cxI = gen_constant positive_modules "xI"
-let cxO = gen_constant positive_modules "xO"
-let cxH = gen_constant positive_modules "xH"
-let ceqbP = gen_constant positive_modules "eqb"
+let positive_prefix = "num.pos"
+let positive_gc = gc positive_prefix
+let cpositive = positive_gc "type"
+let cxI = positive_gc "xI"
+let cxO = positive_gc "xO"
+let cxH = positive_gc "xH"
+let ceqbP = positive_gc "eqb"
 
 (* N *)
-let n_modules = [["Coq";"NArith";"BinNat";"N"]]
-
-let cN = gen_constant positive_modules "N"
-let cN0 = gen_constant positive_modules "N0"
-let cNpos = gen_constant positive_modules "Npos"
-
-let cof_nat = gen_constant n_modules "of_nat"
-
+let n_prefix = "num.N"
+let n_gc = gc n_prefix
+let cN = n_gc "type"
+let cN0 = n_gc "N0"
+let cNpos = n_gc "Npos"
+let cof_nat = n_gc "of_nat"
 
 (* Z *)
-let z_modules = [["Coq";"Numbers";"BinNums"];
-                 ["Coq";"ZArith";"BinInt"];
-                 ["Coq";"ZArith";"BinInt";"Z"]]
-
-let cZ = gen_constant z_modules "Z"
-let cZ0 = gen_constant z_modules "Z0"
-let cZpos = gen_constant z_modules "Zpos"
-let cZneg = gen_constant z_modules "Zneg"
-let copp = gen_constant z_modules "opp"
-let cadd = gen_constant z_modules "add"
-let csub = gen_constant z_modules "sub"
-let cmul = gen_constant z_modules "mul"
-let cltb = gen_constant z_modules "ltb"
-let cleb = gen_constant z_modules "leb"
-let cgeb = gen_constant z_modules "geb"
-let cgtb = gen_constant z_modules "gtb"
-let ceqbZ = gen_constant z_modules "eqb"
-(* let cZeqbsym = gen_constant z_modules "eqb_sym" *)
+let z_prefix = "num.Z"
+let z_gc = gc z_prefix
+let cZ = z_gc "type"
+let cZ0 = z_gc "Z0"
+let cZpos = z_gc "Zpos"
+let cZneg = z_gc "Zneg"
+let copp = z_gc "opp"
+let cadd = z_gc "add"
+let csub = z_gc "sub"
+let cmul = z_gc "mul"
+let cltb = z_gc "ltb"
+let cleb = z_gc "leb"
+let cgeb = z_gc "geb"
+let cgtb = z_gc "gtb"
+let ceqbZ = z_gc "eqb"
 
 (* Booleans *)
-let bool_modules = [["Coq";"Bool";"Bool"]]
-
-let cbool = gen_constant CoqInterface.init_modules "bool"
-let ctrue = gen_constant CoqInterface.init_modules "true"
-let cfalse = gen_constant CoqInterface.init_modules "false"
-let candb = gen_constant CoqInterface.init_modules "andb"
-let corb = gen_constant CoqInterface.init_modules "orb"
-let cxorb = gen_constant CoqInterface.init_modules "xorb"
-let cnegb = gen_constant CoqInterface.init_modules "negb"
-let cimplb = gen_constant CoqInterface.init_modules "implb"
-let ceqb = gen_constant  bool_modules "eqb"
-let cifb = gen_constant bool_modules "ifb"
-let ciff = gen_constant CoqInterface.init_modules "iff"
-let creflect = gen_constant bool_modules "reflect"
+let bool_prefix = "core.bool"
+let bool_gc = gc bool_prefix
+let cbool = bool_gc "type"
+let ctrue = bool_gc "true"
+let cfalse = bool_gc "false"
+let candb = bool_gc "andb"
+let corb = bool_gc "orb"
+let cxorb = bool_gc "xorb"
+let cnegb = bool_gc "negb"
+let cimplb = bool_gc "implb"
+let ceqb = bool_gc "eqb"
+let cifb = bool_gc "ifb"
+let creflect = bool_gc "reflect"
 
 (* Lists *)
-let clist = gen_constant CoqInterface.init_modules "list"
-let cnil = gen_constant CoqInterface.init_modules "nil"
-let ccons = gen_constant CoqInterface.init_modules "cons"
-let clength = gen_constant CoqInterface.init_modules "length"
+let list_prefix = "core.list"
+let list_gc = gc list_prefix
+let clist = list_gc "type"
+let cnil = list_gc "nil"
+let ccons = list_gc "cons"
+let clength = list_gc "length"
 
 (* Option *)
-let coption = gen_constant CoqInterface.init_modules "option"
-let cSome = gen_constant CoqInterface.init_modules "Some"
-let cNone = gen_constant CoqInterface.init_modules "None"
+let option_prefix = "core.option"
+let option_gc = gc option_prefix
+let coption = option_gc "type"
+let cSome = option_gc "Some"
+let cNone = option_gc "None"
 
 (* Pairs *)
-let cpair = gen_constant CoqInterface.init_modules "pair"
-let cprod = gen_constant CoqInterface.init_modules "prod"
+let pair_prefix = "core.prod"
+let pair_gc = gc pair_prefix
+let cpair = pair_gc "intro"
+let cprod = pair_gc "type"
 
 (* Dependent pairs *)
-let csigT = gen_constant CoqInterface.init_modules "sigT"
-(* let cprojT1 = gen_constant CoqInterface.init_modules "projT1" *)
-(* let cprojT2 = gen_constant CoqInterface.init_modules "projT2" *)
-(* let cprojT3 = gen_constant CoqInterface.init_modules "projT3" *)
-
-(* let csigT2 = gen_constant CoqInterface.init_modules "sigT2" *)
-(* let csigT_of_sigT2 = gen_constant CoqInterface.init_modules "sigT_of_sigT2" *)
+let sigT_prefix = "core.sigT"
+let sigT_gc = gc sigT_prefix
+let csigT = sigT_gc "type"
 
 (* Logical Operators *)
-let cnot = gen_constant CoqInterface.init_modules "not"
-let ceq = gen_constant CoqInterface.init_modules "eq"
-let crefl_equal = gen_constant CoqInterface.init_modules "eq_refl"
-let cconj = gen_constant CoqInterface.init_modules "conj"
-let cand = gen_constant CoqInterface.init_modules "and"
+let cnot = gc "core.not" "type"
+let cconj = gc "core.and" "conj"
+let cand = gc "core.and" "type"
+let ciff = gc "core.iff" "type"
+
+(* Equality *)
+let eq_prefix = "core.eq"
+let eq_gc = gc eq_prefix
+let ceq = eq_gc "type"
+let crefl_equal = eq_gc "refl"
+
+(* Micromega *)
+let micromega_prefix = "micromega.ZMicromega"
+let micromega_gc = gc micromega_prefix
+let micromega_coq_proofTerm = micromega_gc "ZArithProof"
 
 (* Bit vectors *)
-let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]]
-let cbitvector = gen_constant bv_modules "bitvector"
-let cof_bits = gen_constant bv_modules "of_bits"
-(* let c_of_bits = gen_constant bv_modules "_of_bits" *)
-let cbitOf = gen_constant bv_modules "bitOf"
-let cbv_eq = gen_constant bv_modules "bv_eq"
-let cbv_not = gen_constant bv_modules "bv_not"
-let cbv_neg = gen_constant bv_modules "bv_neg"
-let cbv_and = gen_constant bv_modules "bv_and"
-let cbv_or = gen_constant bv_modules "bv_or"
-let cbv_xor = gen_constant bv_modules "bv_xor"
-let cbv_add = gen_constant bv_modules "bv_add"
-let cbv_mult = gen_constant bv_modules "bv_mult"
-let cbv_ult = gen_constant bv_modules "bv_ult"
-let cbv_slt = gen_constant bv_modules "bv_slt"
-let cbv_concat = gen_constant bv_modules "bv_concat"
-let cbv_extr = gen_constant bv_modules "bv_extr"
-let cbv_zextn = gen_constant bv_modules "bv_zextn"
-let cbv_sextn = gen_constant bv_modules "bv_sextn"
-let cbv_shl = gen_constant bv_modules "bv_shl"
-let cbv_shr = gen_constant bv_modules "bv_shr"
-
+let bv_prefix = "SMTCoq.bva.BVList.BITVECTOR_LIST"
+let bv_gc = gc bv_prefix
+let cbitvector = bv_gc "bitvector"
+let cof_bits = bv_gc "of_bits"
+let cbitOf = bv_gc "bitOf"
+let cbv_eq = bv_gc "bv_eq"
+let cbv_not = bv_gc "bv_not"
+let cbv_neg = bv_gc "bv_neg"
+let cbv_and = bv_gc "bv_and"
+let cbv_or = bv_gc "bv_or"
+let cbv_xor = bv_gc "bv_xor"
+let cbv_add = bv_gc "bv_add"
+let cbv_mult = bv_gc "bv_mult"
+let cbv_ult = bv_gc "bv_ult"
+let cbv_slt = bv_gc "bv_slt"
+let cbv_concat = bv_gc "bv_concat"
+let cbv_extr = bv_gc "bv_extr"
+let cbv_zextn = bv_gc "bv_zextn"
+let cbv_sextn = bv_gc "bv_sextn"
+let cbv_shl = bv_gc "bv_shl"
+let cbv_shr = bv_gc "bv_shr"
 
 (* Arrays *)
-let array_modules = [["SMTCoq";"array";"FArray"]]
-let cfarray = gen_constant array_modules "FArray.farray"
-let cselect = gen_constant array_modules "select"
-let cstore = gen_constant array_modules "store"
-let cdiff = gen_constant array_modules "diff"
-let cequalarray = gen_constant array_modules "FArray.equal"
-
-(* OrderedType *)
-(* let cOrderedTypeCompare =
- *   gen_constant [["Coq";"Structures";"OrderedType"]] "Compare" *)
-
-(* SMT_terms *)
-let smt_modules = [ ["SMTCoq";"Misc"];
-		    ["SMTCoq";"State"];
-		    ["SMTCoq";"SMT_terms"];
-		    ["SMTCoq";"SMT_terms";"Typ"];
-		    ["SMTCoq";"SMT_terms";"Form"];
-		    ["SMTCoq";"SMT_terms";"Atom"]
-		  ]
-
-let cState_C_t = gen_constant [["SMTCoq";"State";"C"]] "t"
-let cState_S_t = gen_constant [["SMTCoq";"State";"S"]] "t"
-
-let cdistinct = gen_constant smt_modules "distinct"
-
-let ctype = gen_constant smt_modules "type"
-let cTZ = gen_constant smt_modules "TZ"
-let cTbool = gen_constant smt_modules "Tbool"
-let cTpositive = gen_constant smt_modules "Tpositive"
-let cTBV = gen_constant smt_modules "TBV"
-let cTFArray = gen_constant smt_modules "TFArray"
-let cTindex = gen_constant smt_modules "Tindex"
-
-(* let ct_i = gen_constant smt_modules "t_i" *)
-let cinterp_t = gen_constant smt_modules "Typ.interp"
-let cdec_interp = gen_constant smt_modules "dec_interp"
-let cord_interp = gen_constant smt_modules "ord_interp"
-let ccomp_interp = gen_constant smt_modules "comp_interp"
-let cinh_interp = gen_constant smt_modules "inh_interp"
-
-let cinterp_eqb = gen_constant smt_modules "i_eqb"
-(* let cinterp_eqb_eqb = gen_constant smt_modules "i_eqb_eqb" *)
-
-let classes_modules = [["SMTCoq";"classes";"SMT_classes"];
-                       ["SMTCoq";"classes";"SMT_classes_instances"]]
-
-let ctyp_compdec = gen_constant classes_modules "typ_compdec"
-let cTyp_compdec = gen_constant classes_modules "Typ_compdec"
-(* let ctyp_compdec_from = gen_constant classes_modules "typ_compdec_from" *)
-let cunit_typ_compdec = gen_constant classes_modules "unit_typ_compdec"
-let cte_carrier = gen_constant classes_modules "te_carrier"
-let cte_compdec = gen_constant classes_modules "te_compdec"
-let ceqb_of_compdec = gen_constant classes_modules "eqb_of_compdec"
-let cCompDec = gen_constant classes_modules "CompDec"
-
-let cbool_compdec = gen_constant classes_modules "bool_compdec"
-let cZ_compdec = gen_constant classes_modules "Z_compdec"
-let cPositive_compdec = gen_constant classes_modules "Positive_compdec"
-let cBV_compdec = gen_constant classes_modules "BV_compdec"
-let cFArray_compdec = gen_constant classes_modules "FArray_compdec"
-
-let ctval =  gen_constant smt_modules "tval"
-let cTval =  gen_constant smt_modules "Tval"
-
-let cCO_xH = gen_constant smt_modules "CO_xH"
-let cCO_Z0 = gen_constant smt_modules "CO_Z0"
-let cCO_BV = gen_constant smt_modules "CO_BV"
-
-let cUO_xO = gen_constant smt_modules "UO_xO"
-let cUO_xI = gen_constant smt_modules "UO_xI"
-let cUO_Zpos = gen_constant smt_modules "UO_Zpos"
-let cUO_Zneg = gen_constant smt_modules "UO_Zneg"
-let cUO_Zopp = gen_constant smt_modules "UO_Zopp"
-let cUO_BVbitOf = gen_constant smt_modules "UO_BVbitOf"
-let cUO_BVnot = gen_constant smt_modules "UO_BVnot"
-let cUO_BVneg = gen_constant smt_modules "UO_BVneg"
-let cUO_BVextr = gen_constant smt_modules "UO_BVextr"
-let cUO_BVzextn = gen_constant smt_modules "UO_BVzextn"
-let cUO_BVsextn = gen_constant smt_modules "UO_BVsextn"
-
-let cBO_Zplus = gen_constant smt_modules "BO_Zplus"
-let cBO_Zminus = gen_constant smt_modules "BO_Zminus"
-let cBO_Zmult = gen_constant smt_modules "BO_Zmult"
-let cBO_Zlt = gen_constant smt_modules "BO_Zlt"
-let cBO_Zle = gen_constant smt_modules "BO_Zle"
-let cBO_Zge = gen_constant smt_modules "BO_Zge"
-let cBO_Zgt = gen_constant smt_modules "BO_Zgt"
-let cBO_eq = gen_constant smt_modules "BO_eq"
-let cBO_BVand = gen_constant smt_modules "BO_BVand"
-let cBO_BVor = gen_constant smt_modules "BO_BVor"
-let cBO_BVxor = gen_constant smt_modules "BO_BVxor"
-let cBO_BVadd = gen_constant smt_modules "BO_BVadd"
-let cBO_BVmult = gen_constant smt_modules "BO_BVmult"
-let cBO_BVult = gen_constant smt_modules "BO_BVult"
-let cBO_BVslt = gen_constant smt_modules "BO_BVslt"
-let cBO_BVconcat = gen_constant smt_modules "BO_BVconcat"
-let cBO_BVshl = gen_constant smt_modules "BO_BVshl"
-let cBO_BVshr = gen_constant smt_modules "BO_BVshr"
-let cBO_select = gen_constant smt_modules "BO_select"
-let cBO_diffarray = gen_constant smt_modules "BO_diffarray"
-
-let cTO_store = gen_constant smt_modules "TO_store"
-
-let cNO_distinct = gen_constant smt_modules "NO_distinct"
-
-let catom = gen_constant smt_modules "atom"
-let cAcop = gen_constant smt_modules "Acop"
-let cAuop = gen_constant smt_modules "Auop"
-let cAbop = gen_constant smt_modules "Abop"
-let cAtop = gen_constant smt_modules "Atop"
-let cAnop = gen_constant smt_modules "Anop"
-let cAapp = gen_constant smt_modules "Aapp"
-
-let cform  = gen_constant smt_modules "form"
-let cFatom = gen_constant smt_modules "Fatom"
-let cFtrue = gen_constant smt_modules "Ftrue"
-let cFfalse = gen_constant smt_modules "Ffalse"
-let cFnot2 = gen_constant smt_modules "Fnot2"
-let cFand = gen_constant smt_modules "Fand"
-let cFor = gen_constant smt_modules "For"
-let cFxor = gen_constant smt_modules "Fxor"
-let cFimp = gen_constant smt_modules "Fimp"
-let cFiff = gen_constant smt_modules "Fiff"
-let cFite = gen_constant smt_modules "Fite"
-let cFbbT = gen_constant smt_modules "FbbT"
-
-let cvalid_sat_checker = gen_constant [["SMTCoq";"Trace";"Sat_Checker"]] "valid"
-let cinterp_var_sat_checker = gen_constant [["SMTCoq";"Trace";"Sat_Checker"]] "interp_var"
-
-let make_certif_ops modules args =
+let array_prefix = "SMTCoq.array.FArray"
+let array_gc = gc array_prefix
+let cfarray = array_gc "farray"
+let cselect = array_gc "select"
+let cstore = array_gc "store"
+let cdiff = array_gc "diff"
+let cequalarray = array_gc "equal"
+
+(* SMTCoq terms *)
+let state_prefix = "SMTCoq.State"
+let state_gc = gc state_prefix
+let cState_C_t = state_gc "C.t"
+let cState_S_t = state_gc "S.t"
+
+let misc_prefix = "SMTCoq.Misc"
+let misc_gc = gc misc_prefix
+let cdistinct = misc_gc "distinct"
+
+let terms_prefix = "SMTCoq.SMT_terms"
+let terms_gc = gc terms_prefix
+
+let ctype = terms_gc "Typ.type"
+let cTZ = terms_gc "Typ.TZ"
+let cTbool = terms_gc "Typ.Tbool"
+let cTpositive = terms_gc "Typ.Tpositive"
+let cTBV = terms_gc "Typ.TBV"
+let cTFArray = terms_gc "Typ.TFArray"
+let cTindex = terms_gc "Typ.Tindex"
+
+let cinterp_t = terms_gc "Typ.interp"
+let cdec_interp = terms_gc "Typ.dec_interp"
+let cord_interp = terms_gc "Typ.ord_interp"
+let ccomp_interp = terms_gc "Typ.comp_interp"
+let cinh_interp = terms_gc "Typ.inh_interp"
+
+let cinterp_eqb = terms_gc "Typ.i_eqb"
+
+let ctval =  terms_gc "Atom.tval"
+let cTval =  terms_gc "Atom.Tval"
+
+let cCO_xH = terms_gc "Atom.CO_xH"
+let cCO_Z0 = terms_gc "Atom.CO_Z0"
+let cCO_BV = terms_gc "Atom.CO_BV"
+
+let cUO_xO = terms_gc "Atom.UO_xO"
+let cUO_xI = terms_gc "Atom.UO_xI"
+let cUO_Zpos = terms_gc "Atom.UO_Zpos"
+let cUO_Zneg = terms_gc "Atom.UO_Zneg"
+let cUO_Zopp = terms_gc "Atom.UO_Zopp"
+let cUO_BVbitOf = terms_gc "Atom.UO_BVbitOf"
+let cUO_BVnot = terms_gc "Atom.UO_BVnot"
+let cUO_BVneg = terms_gc "Atom.UO_BVneg"
+let cUO_BVextr = terms_gc "Atom.UO_BVextr"
+let cUO_BVzextn = terms_gc "Atom.UO_BVzextn"
+let cUO_BVsextn = terms_gc "Atom.UO_BVsextn"
+
+let cBO_Zplus = terms_gc "Atom.BO_Zplus"
+let cBO_Zminus = terms_gc "Atom.BO_Zminus"
+let cBO_Zmult = terms_gc "Atom.BO_Zmult"
+let cBO_Zlt = terms_gc "Atom.BO_Zlt"
+let cBO_Zle = terms_gc "Atom.BO_Zle"
+let cBO_Zge = terms_gc "Atom.BO_Zge"
+let cBO_Zgt = terms_gc "Atom.BO_Zgt"
+let cBO_eq = terms_gc "Atom.BO_eq"
+let cBO_BVand = terms_gc "Atom.BO_BVand"
+let cBO_BVor = terms_gc "Atom.BO_BVor"
+let cBO_BVxor = terms_gc "Atom.BO_BVxor"
+let cBO_BVadd = terms_gc "Atom.BO_BVadd"
+let cBO_BVmult = terms_gc "Atom.BO_BVmult"
+let cBO_BVult = terms_gc "Atom.BO_BVult"
+let cBO_BVslt = terms_gc "Atom.BO_BVslt"
+let cBO_BVconcat = terms_gc "Atom.BO_BVconcat"
+let cBO_BVshl = terms_gc "Atom.BO_BVshl"
+let cBO_BVshr = terms_gc "Atom.BO_BVshr"
+let cBO_select = terms_gc "Atom.BO_select"
+let cBO_diffarray = terms_gc "Atom.BO_diffarray"
+
+let cTO_store = terms_gc "Atom.TO_store"
+
+let cNO_distinct = terms_gc "Atom.NO_distinct"
+
+let catom = terms_gc "Atom.atom"
+let cAcop = terms_gc "Atom.Acop"
+let cAuop = terms_gc "Atom.Auop"
+let cAbop = terms_gc "Atom.Abop"
+let cAtop = terms_gc "Atom.Atop"
+let cAnop = terms_gc "Atom.Anop"
+let cAapp = terms_gc "Atom.Aapp"
+
+let cform  = terms_gc "Form.form"
+let cFatom = terms_gc "Form.Fatom"
+let cFtrue = terms_gc "Form.Ftrue"
+let cFfalse = terms_gc "Form.Ffalse"
+let cFnot2 = terms_gc "Form.Fnot2"
+let cFand = terms_gc "Form.Fand"
+let cFor = terms_gc "Form.For"
+let cFxor = terms_gc "Form.Fxor"
+let cFimp = terms_gc "Form.Fimp"
+let cFiff = terms_gc "Form.Fiff"
+let cFite = terms_gc "Form.Fite"
+let cFbbT = terms_gc "Form.FbbT"
+
+(* SMTCoq Classes *)
+let classes_prefix = "SMTCoq.classes.SMT_classes"
+let classes_gc = gc classes_prefix
+let ctyp_compdec = classes_gc "typ_compdec"
+let cTyp_compdec = classes_gc "Typ_compdec"
+let cte_carrier = classes_gc "te_carrier"
+let cte_compdec = classes_gc "te_compdec"
+let ceqb_of_compdec = classes_gc "eqb_of_compdec"
+let cCompDec = classes_gc "CompDec"
+
+let classesi_prefix = "SMTCoq.classes.SMT_classes_instances"
+let classesi_gc = gc classesi_prefix
+let cunit_typ_compdec = classesi_gc "unit_typ_compdec"
+let cbool_compdec = classesi_gc "bool_compdec"
+let cZ_compdec = classesi_gc "Z_compdec"
+let cPositive_compdec = classesi_gc "Positive_compdec"
+let cBV_compdec = classesi_gc "BV_compdec"
+let cFArray_compdec = classesi_gc "FArray_compdec"
+
+(* SMTCoq Trace *)
+let sat_checker_prefix = "SMTCoq.Trace.Sat_Checker"
+let sat_checker_gc = gc sat_checker_prefix
+let csat_checker_valid = sat_checker_gc "valid"
+let csat_checker_interp_var = sat_checker_gc "interp_var"
+let csat_checker_Certif = sat_checker_gc "Certif"
+let csat_checker_dimacs = sat_checker_gc "dimacs"
+let csat_checker_certif = sat_checker_gc "certif"
+let csat_checker_theorem_checker = sat_checker_gc "theorem_checker"
+let csat_checker_checker = sat_checker_gc "checker"
+
+let cnf_checker_prefix = "SMTCoq.Trace.Cnf_Checker"
+let cnf_checker_gc = gc cnf_checker_prefix
+let ccnf_checker_certif = cnf_checker_gc "certif"
+let ccnf_checker_Certif = cnf_checker_gc "Certif"
+let ccnf_checker_checker_b_correct = cnf_checker_gc "checker_b_correct"
+let ccnf_checker_checker_b = cnf_checker_gc "checker_b"
+let ccnf_checker_checker_eq_correct = cnf_checker_gc "checker_eq_correct"
+let ccnf_checker_checker_eq = cnf_checker_gc "checker_eq"
+
+let euf_checker_prefix = "SMTCoq.Trace.Euf_Checker"
+let euf_checker_gc = gc euf_checker_prefix
+let ceuf_checker_Certif = euf_checker_gc "Certif"
+let ceuf_checker_certif = euf_checker_gc "certif"
+let ceuf_checker_checker = euf_checker_gc "checker"
+let ceuf_checker_checker_correct = euf_checker_gc "checker_correct"
+let ceuf_checker_checker_b_correct = euf_checker_gc "checker_b_correct"
+let ceuf_checker_checker_b = euf_checker_gc "checker_b"
+let ceuf_checker_checker_eq_correct = euf_checker_gc "checker_eq_correct"
+let ceuf_checker_checker_eq = euf_checker_gc "checker_eq"
+let ceuf_checker_checker_debug = euf_checker_gc "checker_debug"
+let ceuf_checker_name_step = euf_checker_gc "name_step"
+let ceuf_checker_Name_Res = euf_checker_gc "Name_Res"
+let ceuf_checker_Name_Weaken = euf_checker_gc "Name_Weaken"
+let ceuf_checker_Name_ImmFlatten = euf_checker_gc "Name_ImmFlatten"
+let ceuf_checker_Name_CTrue = euf_checker_gc "Name_CTrue"
+let ceuf_checker_Name_CFalse = euf_checker_gc "Name_CFalse"
+let ceuf_checker_Name_BuildDef = euf_checker_gc "Name_BuildDef"
+let ceuf_checker_Name_BuildDef2 = euf_checker_gc "Name_BuildDef2"
+let ceuf_checker_Name_BuildProj = euf_checker_gc "Name_BuildProj"
+let ceuf_checker_Name_ImmBuildDef = euf_checker_gc "Name_ImmBuildDef"
+let ceuf_checker_Name_ImmBuildDef2 = euf_checker_gc "Name_ImmBuildDef2"
+let ceuf_checker_Name_ImmBuildProj = euf_checker_gc "Name_ImmBuildProj"
+let ceuf_checker_Name_EqTr = euf_checker_gc "Name_EqTr"
+let ceuf_checker_Name_EqCgr = euf_checker_gc "Name_EqCgr"
+let ceuf_checker_Name_EqCgrP = euf_checker_gc "Name_EqCgrP"
+let ceuf_checker_Name_LiaMicromega = euf_checker_gc "Name_LiaMicromega"
+let ceuf_checker_Name_LiaDiseq = euf_checker_gc "Name_LiaDiseq"
+let ceuf_checker_Name_SplArith = euf_checker_gc "Name_SplArith"
+let ceuf_checker_Name_SplDistinctElim = euf_checker_gc "Name_SplDistinctElim"
+let ceuf_checker_Name_BBVar = euf_checker_gc "Name_BBVar"
+let ceuf_checker_Name_BBConst = euf_checker_gc "Name_BBConst"
+let ceuf_checker_Name_BBOp = euf_checker_gc "Name_BBOp"
+let ceuf_checker_Name_BBNot = euf_checker_gc "Name_BBNot"
+let ceuf_checker_Name_BBNeg = euf_checker_gc "Name_BBNeg"
+let ceuf_checker_Name_BBAdd = euf_checker_gc "Name_BBAdd"
+let ceuf_checker_Name_BBConcat = euf_checker_gc "Name_BBConcat"
+let ceuf_checker_Name_BBMul = euf_checker_gc "Name_BBMul"
+let ceuf_checker_Name_BBUlt = euf_checker_gc "Name_BBUlt"
+let ceuf_checker_Name_BBSlt = euf_checker_gc "Name_BBSlt"
+let ceuf_checker_Name_BBEq = euf_checker_gc "Name_BBEq"
+let ceuf_checker_Name_BBDiseq = euf_checker_gc "Name_BBDiseq"
+let ceuf_checker_Name_BBExtract = euf_checker_gc "Name_BBExtract"
+let ceuf_checker_Name_BBZextend = euf_checker_gc "Name_BBZextend"
+let ceuf_checker_Name_BBSextend = euf_checker_gc "Name_BBSextend"
+let ceuf_checker_Name_BBShl = euf_checker_gc "Name_BBShl"
+let ceuf_checker_Name_BBShr = euf_checker_gc "Name_BBShr"
+let ceuf_checker_Name_RowEq = euf_checker_gc "Name_RowEq"
+let ceuf_checker_Name_RowNeq = euf_checker_gc "Name_RowNeq"
+let ceuf_checker_Name_Ext = euf_checker_gc "Name_Ext"
+let ceuf_checker_Name_Hole = euf_checker_gc "Name_Hole"
+
+type certif_ops =
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm
+let make_certif_ops prefix args =
+  let gc = gc prefix in
   let gen_constant c =
     match args with
-      | Some args -> lazy (mklApp (gen_constant modules c) args)
-      | None -> gen_constant modules c in
+      | Some args -> lazy (mklApp (gc c) args)
+      | None -> gc c in
  (gen_constant "step",
   gen_constant "Res", gen_constant "Weaken", gen_constant "ImmFlatten",
   gen_constant "CTrue", gen_constant "CFalse",
   gen_constant "BuildDef", gen_constant "BuildDef2",
   gen_constant "BuildProj",
-  gen_constant "ImmBuildProj", gen_constant"ImmBuildDef",
+  gen_constant "ImmBuildProj", gen_constant "ImmBuildDef",
   gen_constant"ImmBuildDef2",
   gen_constant "EqTr", gen_constant "EqCgr", gen_constant "EqCgrP",
   gen_constant "LiaMicromega", gen_constant "LiaDiseq",
@@ -296,6 +391,9 @@ let make_certif_ops modules args =
   gen_constant "BBShl", gen_constant "BBShr",
   gen_constant "RowEq", gen_constant "RowNeq", gen_constant "Ext",
   gen_constant "Hole", gen_constant "ForallInst")
+let csat_checker_certif_ops = make_certif_ops sat_checker_prefix None
+let ccnf_checker_certif_ops = make_certif_ops cnf_checker_prefix None
+let ceuf_checker_certif_ops = make_certif_ops euf_checker_prefix
 
 
 (** Useful constructions *)
@@ -352,6 +450,19 @@ let rec mk_bv_list = function
   | b :: bv ->
     mklApp ccons [|Lazy.force cbool; mkBool b; mk_bv_list bv|]
 
+(* Compute an array *)
+let mkArray : Constr.types * Constr.t array -> Constr.t =
+  fun (ty, a) ->
+  let l = (Array.length a) - 1 in
+  snd (Array.fold_left (fun (i,acc) c ->
+                        let acc' =
+                          if i = l then
+                            acc
+                          else
+                            mklApp cset [|ty; acc; mkInt i; c|] in
+                        (i+1,acc')
+                       ) (0, mklApp cmake [|ty; mkInt l; a.(l)|]) a)
+
 
 (* Reification *)
 let mk_bool b =
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index 92acbb6..b5b1a0b 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -10,249 +10,322 @@
 (**************************************************************************)
 
 
-val gen_constant : string list list -> string -> CoqInterface.constr lazy_t
+type coqTerm = CoqInterface.constr lazy_t
 
 (* Int63 *)
-val cint : CoqInterface.constr lazy_t
-val ceq63 : CoqInterface.constr lazy_t
+val cint : coqTerm
+val ceq63 : coqTerm
 
 (* PArray *)
-val carray : CoqInterface.constr lazy_t
+val carray : coqTerm
+val cmake : coqTerm
+val cset : coqTerm
+
+(* is_true *)
+val cis_true : coqTerm
 
 (* nat *)
-val cnat : CoqInterface.constr lazy_t
-val cO : CoqInterface.constr lazy_t
-val cS : CoqInterface.constr lazy_t
+val cnat : coqTerm
+val cO : coqTerm
+val cS : coqTerm
 
 (* Positive *)
-val cpositive : CoqInterface.constr lazy_t
-val cxI : CoqInterface.constr lazy_t
-val cxO : CoqInterface.constr lazy_t
-val cxH : CoqInterface.constr lazy_t
-val ceqbP : CoqInterface.constr lazy_t
+val cpositive : coqTerm
+val cxI : coqTerm
+val cxO : coqTerm
+val cxH : coqTerm
+val ceqbP : coqTerm
 
 (* N *)
-val cN : CoqInterface.constr lazy_t
-val cN0 : CoqInterface.constr lazy_t
-val cNpos : CoqInterface.constr lazy_t
-val cof_nat : CoqInterface.constr lazy_t
+val cN : coqTerm
+val cN0 : coqTerm
+val cNpos : coqTerm
+val cof_nat : coqTerm
 
 (* Z *)
-val cZ : CoqInterface.constr lazy_t
-val cZ0 : CoqInterface.constr lazy_t
-val cZpos : CoqInterface.constr lazy_t
-val cZneg : CoqInterface.constr lazy_t
-val copp : CoqInterface.constr lazy_t
-val cadd : CoqInterface.constr lazy_t
-val csub : CoqInterface.constr lazy_t
-val cmul : CoqInterface.constr lazy_t
-val cltb : CoqInterface.constr lazy_t
-val cleb : CoqInterface.constr lazy_t
-val cgeb : CoqInterface.constr lazy_t
-val cgtb : CoqInterface.constr lazy_t
-val ceqbZ : CoqInterface.constr lazy_t
+val cZ : coqTerm
+val cZ0 : coqTerm
+val cZpos : coqTerm
+val cZneg : coqTerm
+val copp : coqTerm
+val cadd : coqTerm
+val csub : coqTerm
+val cmul : coqTerm
+val cltb : coqTerm
+val cleb : coqTerm
+val cgeb : coqTerm
+val cgtb : coqTerm
+val ceqbZ : coqTerm
 
 (* Booleans *)
-val cbool : CoqInterface.constr lazy_t
-val ctrue : CoqInterface.constr lazy_t
-val cfalse : CoqInterface.constr lazy_t
-val candb : CoqInterface.constr lazy_t
-val corb : CoqInterface.constr lazy_t
-val cxorb : CoqInterface.constr lazy_t
-val cnegb : CoqInterface.constr lazy_t
-val cimplb : CoqInterface.constr lazy_t
-val ceqb : CoqInterface.constr lazy_t
-val cifb : CoqInterface.constr lazy_t
-val ciff : CoqInterface.constr lazy_t
-val creflect : CoqInterface.constr lazy_t
+val cbool : coqTerm
+val ctrue : coqTerm
+val cfalse : coqTerm
+val candb : coqTerm
+val corb : coqTerm
+val cxorb : coqTerm
+val cnegb : coqTerm
+val cimplb : coqTerm
+val ceqb : coqTerm
+val cifb : coqTerm
+val creflect : coqTerm
 
 (* Lists *)
-val clist : CoqInterface.constr lazy_t
-val cnil : CoqInterface.constr lazy_t
-val ccons : CoqInterface.constr lazy_t
-val clength : CoqInterface.constr lazy_t
+val clist : coqTerm
+val cnil : coqTerm
+val ccons : coqTerm
+val clength : coqTerm
 
 (* Option *)
-val coption : CoqInterface.constr lazy_t
-val cSome : CoqInterface.constr lazy_t
-val cNone : CoqInterface.constr lazy_t
+val coption : coqTerm
+val cSome : coqTerm
+val cNone : coqTerm
 
 (* Pairs *)
-val cpair : CoqInterface.constr lazy_t
-val cprod : CoqInterface.constr lazy_t
+val cpair : coqTerm
+val cprod : coqTerm
 
 (* Dependent pairs *)
-val csigT : CoqInterface.constr lazy_t
+val csigT : coqTerm
 
 (* Logical Operators *)
-val cnot : CoqInterface.constr lazy_t
-val ceq : CoqInterface.constr lazy_t
-val crefl_equal : CoqInterface.constr lazy_t
-val cconj : CoqInterface.constr lazy_t
-val cand : CoqInterface.constr lazy_t
+val cnot : coqTerm
+val cconj : coqTerm
+val cand : coqTerm
+val ciff : coqTerm
+
+(* Equality *)
+val ceq : coqTerm
+val crefl_equal : coqTerm
+
+(* Micromega *)
+val micromega_coq_proofTerm : coqTerm
 
 (* Bit vectors *)
-val cbitvector : CoqInterface.constr lazy_t
-val cof_bits : CoqInterface.constr lazy_t
-val cbitOf : CoqInterface.constr lazy_t
-val cbv_eq : CoqInterface.constr lazy_t
-val cbv_not : CoqInterface.constr lazy_t
-val cbv_neg : CoqInterface.constr lazy_t
-val cbv_and : CoqInterface.constr lazy_t
-val cbv_or : CoqInterface.constr lazy_t
-val cbv_xor : CoqInterface.constr lazy_t
-val cbv_add : CoqInterface.constr lazy_t
-val cbv_mult : CoqInterface.constr lazy_t
-val cbv_ult : CoqInterface.constr lazy_t
-val cbv_slt : CoqInterface.constr lazy_t
-val cbv_concat : CoqInterface.constr lazy_t
-val cbv_extr : CoqInterface.constr lazy_t
-val cbv_zextn : CoqInterface.constr lazy_t
-val cbv_sextn : CoqInterface.constr lazy_t
-val cbv_shl : CoqInterface.constr lazy_t
-val cbv_shr : CoqInterface.constr lazy_t
+val cbitvector : coqTerm
+val cof_bits : coqTerm
+val cbitOf : coqTerm
+val cbv_eq : coqTerm
+val cbv_not : coqTerm
+val cbv_neg : coqTerm
+val cbv_and : coqTerm
+val cbv_or : coqTerm
+val cbv_xor : coqTerm
+val cbv_add : coqTerm
+val cbv_mult : coqTerm
+val cbv_ult : coqTerm
+val cbv_slt : coqTerm
+val cbv_concat : coqTerm
+val cbv_extr : coqTerm
+val cbv_zextn : coqTerm
+val cbv_sextn : coqTerm
+val cbv_shl : coqTerm
+val cbv_shr : coqTerm
 
 (* Arrays *)
-val cfarray : CoqInterface.constr lazy_t
-val cselect : CoqInterface.constr lazy_t
-val cstore : CoqInterface.constr lazy_t
-val cdiff : CoqInterface.constr lazy_t
-val cequalarray : CoqInterface.constr lazy_t
-
-(* OrderedType *)
-
-(* SMT_terms *)
-val cState_C_t : CoqInterface.constr lazy_t
-val cState_S_t : CoqInterface.constr lazy_t
-
-val cdistinct : CoqInterface.constr lazy_t
-
-val ctype : CoqInterface.constr lazy_t
-val cTZ : CoqInterface.constr lazy_t
-val cTbool : CoqInterface.constr lazy_t
-val cTpositive : CoqInterface.constr lazy_t
-val cTBV : CoqInterface.constr lazy_t
-val cTFArray : CoqInterface.constr lazy_t
-val cTindex : CoqInterface.constr lazy_t
-
-val cinterp_t : CoqInterface.constr lazy_t
-val cdec_interp : CoqInterface.constr lazy_t
-val cord_interp : CoqInterface.constr lazy_t
-val ccomp_interp : CoqInterface.constr lazy_t
-val cinh_interp : CoqInterface.constr lazy_t
-
-val cinterp_eqb : CoqInterface.constr lazy_t
-
-val ctyp_compdec : CoqInterface.constr lazy_t
-val cTyp_compdec : CoqInterface.constr lazy_t
-val cunit_typ_compdec : CoqInterface.constr lazy_t
-val cte_carrier : CoqInterface.constr lazy_t
-val cte_compdec : CoqInterface.constr lazy_t
-val ceqb_of_compdec : CoqInterface.constr lazy_t
-val cCompDec : CoqInterface.constr lazy_t
-
-val cbool_compdec : CoqInterface.constr lazy_t
-val cZ_compdec : CoqInterface.constr lazy_t
-val cPositive_compdec : CoqInterface.constr lazy_t
-val cBV_compdec : CoqInterface.constr lazy_t
-val cFArray_compdec : CoqInterface.constr lazy_t
-
-val ctval : CoqInterface.constr lazy_t
-val cTval : CoqInterface.constr lazy_t
-
-val cCO_xH : CoqInterface.constr lazy_t
-val cCO_Z0 : CoqInterface.constr lazy_t
-val cCO_BV : CoqInterface.constr lazy_t
-
-val cUO_xO : CoqInterface.constr lazy_t
-val cUO_xI : CoqInterface.constr lazy_t
-val cUO_Zpos : CoqInterface.constr lazy_t
-val cUO_Zneg : CoqInterface.constr lazy_t
-val cUO_Zopp : CoqInterface.constr lazy_t
-val cUO_BVbitOf : CoqInterface.constr lazy_t
-val cUO_BVnot : CoqInterface.constr lazy_t
-val cUO_BVneg : CoqInterface.constr lazy_t
-val cUO_BVextr : CoqInterface.constr lazy_t
-val cUO_BVzextn : CoqInterface.constr lazy_t
-val cUO_BVsextn : CoqInterface.constr lazy_t
-
-val cBO_Zplus : CoqInterface.constr lazy_t
-val cBO_Zminus : CoqInterface.constr lazy_t
-val cBO_Zmult : CoqInterface.constr lazy_t
-val cBO_Zlt : CoqInterface.constr lazy_t
-val cBO_Zle : CoqInterface.constr lazy_t
-val cBO_Zge : CoqInterface.constr lazy_t
-val cBO_Zgt : CoqInterface.constr lazy_t
-val cBO_eq : CoqInterface.constr lazy_t
-val cBO_BVand : CoqInterface.constr lazy_t
-val cBO_BVor : CoqInterface.constr lazy_t
-val cBO_BVxor : CoqInterface.constr lazy_t
-val cBO_BVadd : CoqInterface.constr lazy_t
-val cBO_BVmult : CoqInterface.constr lazy_t
-val cBO_BVult : CoqInterface.constr lazy_t
-val cBO_BVslt : CoqInterface.constr lazy_t
-val cBO_BVconcat : CoqInterface.constr lazy_t
-val cBO_BVshl : CoqInterface.constr lazy_t
-val cBO_BVshr : CoqInterface.constr lazy_t
-val cBO_select : CoqInterface.constr lazy_t
-val cBO_diffarray : CoqInterface.constr lazy_t
-
-val cTO_store : CoqInterface.constr lazy_t
-
-val cNO_distinct : CoqInterface.constr lazy_t
-
-val catom : CoqInterface.constr lazy_t
-val cAcop : CoqInterface.constr lazy_t
-val cAuop : CoqInterface.constr lazy_t
-val cAbop : CoqInterface.constr lazy_t
-val cAtop : CoqInterface.constr lazy_t
-val cAnop : CoqInterface.constr lazy_t
-val cAapp : CoqInterface.constr lazy_t
-
-val cform : CoqInterface.constr lazy_t
-val cFatom : CoqInterface.constr lazy_t
-val cFtrue : CoqInterface.constr lazy_t
-val cFfalse : CoqInterface.constr lazy_t
-val cFnot2 : CoqInterface.constr lazy_t
-val cFand : CoqInterface.constr lazy_t
-val cFor : CoqInterface.constr lazy_t
-val cFxor : CoqInterface.constr lazy_t
-val cFimp : CoqInterface.constr lazy_t
-val cFiff : CoqInterface.constr lazy_t
-val cFite : CoqInterface.constr lazy_t
-val cFbbT : CoqInterface.constr lazy_t
-
-val cis_true : CoqInterface.constr lazy_t
-
-val cvalid_sat_checker : CoqInterface.constr lazy_t
-val cinterp_var_sat_checker : CoqInterface.constr lazy_t
-
-val make_certif_ops :
-           string list list ->
-           CoqInterface.constr array option ->
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t * CoqInterface.constr lazy_t *
-           CoqInterface.constr lazy_t * CoqInterface.constr lazy_t
+val cfarray : coqTerm
+val cselect : coqTerm
+val cstore : coqTerm
+val cdiff : coqTerm
+val cequalarray : coqTerm
+
+(* SMTCoq terms *)
+val cState_C_t : coqTerm
+val cState_S_t : coqTerm
+
+val cdistinct : coqTerm
+
+val ctype : coqTerm
+val cTZ : coqTerm
+val cTbool : coqTerm
+val cTpositive : coqTerm
+val cTBV : coqTerm
+val cTFArray : coqTerm
+val cTindex : coqTerm
+
+val cinterp_t : coqTerm
+val cdec_interp : coqTerm
+val cord_interp : coqTerm
+val ccomp_interp : coqTerm
+val cinh_interp : coqTerm
+
+val cinterp_eqb : coqTerm
+
+val ctval : coqTerm
+val cTval : coqTerm
+
+val cCO_xH : coqTerm
+val cCO_Z0 : coqTerm
+val cCO_BV : coqTerm
+
+val cUO_xO : coqTerm
+val cUO_xI : coqTerm
+val cUO_Zpos : coqTerm
+val cUO_Zneg : coqTerm
+val cUO_Zopp : coqTerm
+val cUO_BVbitOf : coqTerm
+val cUO_BVnot : coqTerm
+val cUO_BVneg : coqTerm
+val cUO_BVextr : coqTerm
+val cUO_BVzextn : coqTerm
+val cUO_BVsextn : coqTerm
+
+val cBO_Zplus : coqTerm
+val cBO_Zminus : coqTerm
+val cBO_Zmult : coqTerm
+val cBO_Zlt : coqTerm
+val cBO_Zle : coqTerm
+val cBO_Zge : coqTerm
+val cBO_Zgt : coqTerm
+val cBO_eq : coqTerm
+val cBO_BVand : coqTerm
+val cBO_BVor : coqTerm
+val cBO_BVxor : coqTerm
+val cBO_BVadd : coqTerm
+val cBO_BVmult : coqTerm
+val cBO_BVult : coqTerm
+val cBO_BVslt : coqTerm
+val cBO_BVconcat : coqTerm
+val cBO_BVshl : coqTerm
+val cBO_BVshr : coqTerm
+val cBO_select : coqTerm
+val cBO_diffarray : coqTerm
+
+val cTO_store : coqTerm
+
+val cNO_distinct : coqTerm
+
+val catom : coqTerm
+val cAcop : coqTerm
+val cAuop : coqTerm
+val cAbop : coqTerm
+val cAtop : coqTerm
+val cAnop : coqTerm
+val cAapp : coqTerm
+
+val cform : coqTerm
+val cFatom : coqTerm
+val cFtrue : coqTerm
+val cFfalse : coqTerm
+val cFnot2 : coqTerm
+val cFand : coqTerm
+val cFor : coqTerm
+val cFxor : coqTerm
+val cFimp : coqTerm
+val cFiff : coqTerm
+val cFite : coqTerm
+val cFbbT : coqTerm
+
+(* SMTCoq Classes *)
+val ctyp_compdec : coqTerm
+val cTyp_compdec : coqTerm
+val cte_carrier : coqTerm
+val cte_compdec : coqTerm
+val ceqb_of_compdec : coqTerm
+val cCompDec : coqTerm
+
+val cunit_typ_compdec : coqTerm
+val cbool_compdec : coqTerm
+val cZ_compdec : coqTerm
+val cPositive_compdec : coqTerm
+val cBV_compdec : coqTerm
+val cFArray_compdec : coqTerm
+
+(* SMTCoq Trace *)
+type certif_ops =
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm * coqTerm *
+  coqTerm * coqTerm
+
+val csat_checker_valid : coqTerm
+val csat_checker_interp_var : coqTerm
+val csat_checker_Certif : coqTerm
+val csat_checker_dimacs : coqTerm
+val csat_checker_certif : coqTerm
+val csat_checker_theorem_checker : coqTerm
+val csat_checker_checker : coqTerm
+val csat_checker_certif_ops : certif_ops
+
+val ccnf_checker_certif : coqTerm
+val ccnf_checker_Certif : coqTerm
+val ccnf_checker_checker_b_correct : coqTerm
+val ccnf_checker_checker_b : coqTerm
+val ccnf_checker_checker_eq_correct : coqTerm
+val ccnf_checker_checker_eq : coqTerm
+val ccnf_checker_certif_ops : certif_ops
+
+val ceuf_checker_Certif : coqTerm
+val ceuf_checker_certif : coqTerm
+val ceuf_checker_checker : coqTerm
+val ceuf_checker_checker_correct : coqTerm
+val ceuf_checker_checker_b_correct : coqTerm
+val ceuf_checker_checker_b : coqTerm
+val ceuf_checker_checker_eq_correct : coqTerm
+val ceuf_checker_checker_eq : coqTerm
+val ceuf_checker_checker_debug : coqTerm
+val ceuf_checker_name_step : coqTerm
+val ceuf_checker_Name_Res : coqTerm
+val ceuf_checker_Name_Weaken : coqTerm
+val ceuf_checker_Name_ImmFlatten : coqTerm
+val ceuf_checker_Name_CTrue : coqTerm
+val ceuf_checker_Name_CFalse : coqTerm
+val ceuf_checker_Name_BuildDef : coqTerm
+val ceuf_checker_Name_BuildDef2 : coqTerm
+val ceuf_checker_Name_BuildProj : coqTerm
+val ceuf_checker_Name_ImmBuildDef : coqTerm
+val ceuf_checker_Name_ImmBuildDef2 : coqTerm
+val ceuf_checker_Name_ImmBuildProj : coqTerm
+val ceuf_checker_Name_EqTr : coqTerm
+val ceuf_checker_Name_EqCgr : coqTerm
+val ceuf_checker_Name_EqCgrP : coqTerm
+val ceuf_checker_Name_LiaMicromega : coqTerm
+val ceuf_checker_Name_LiaDiseq : coqTerm
+val ceuf_checker_Name_SplArith : coqTerm
+val ceuf_checker_Name_SplDistinctElim : coqTerm
+val ceuf_checker_Name_BBVar : coqTerm
+val ceuf_checker_Name_BBConst : coqTerm
+val ceuf_checker_Name_BBOp : coqTerm
+val ceuf_checker_Name_BBNot : coqTerm
+val ceuf_checker_Name_BBNeg : coqTerm
+val ceuf_checker_Name_BBAdd : coqTerm
+val ceuf_checker_Name_BBConcat : coqTerm
+val ceuf_checker_Name_BBMul : coqTerm
+val ceuf_checker_Name_BBUlt : coqTerm
+val ceuf_checker_Name_BBSlt : coqTerm
+val ceuf_checker_Name_BBEq : coqTerm
+val ceuf_checker_Name_BBDiseq : coqTerm
+val ceuf_checker_Name_BBExtract : coqTerm
+val ceuf_checker_Name_BBZextend : coqTerm
+val ceuf_checker_Name_BBSextend : coqTerm
+val ceuf_checker_Name_BBShl : coqTerm
+val ceuf_checker_Name_BBShr : coqTerm
+val ceuf_checker_Name_RowEq : coqTerm
+val ceuf_checker_Name_RowNeq : coqTerm
+val ceuf_checker_Name_Ext : coqTerm
+val ceuf_checker_Name_Hole : coqTerm
+val ceuf_checker_certif_ops : CoqInterface.constr array option -> certif_ops
+
 
 (* Some constructions *)
-val ceq_refl_true : CoqInterface.constr lazy_t
+val ceq_refl_true : coqTerm
 val eq_refl_true : unit -> CoqInterface.constr
 val vm_cast_true_no_check : CoqInterface.constr -> CoqInterface.constr
 val vm_cast_true : Environ.env -> CoqInterface.constr -> CoqInterface.constr
 val mkNat : int -> CoqInterface.constr
 val mkN : int -> CoqInterface.constr
 val mk_bv_list : bool list -> CoqInterface.constr
+val mkArray : Constr.types * Constr.t array -> Constr.t
 
 (* Reification *)
 val mk_bool : CoqInterface.constr -> bool
diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
index 0296c88..ff648a9 100644
--- a/src/trace/satAtom.ml
+++ b/src/trace/satAtom.ml
@@ -51,7 +51,7 @@ module Atom =
       t
 
     let interp_tbl reify =
-      CoqInterface.mkArray (Lazy.force cbool, atom_tbl reify)
+      CoqTerms.mkArray (Lazy.force cbool, atom_tbl reify)
 
     let logic _ = SL.empty
 
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 9697882..6447ae7 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -385,7 +385,7 @@ module Op =
         let index, hval = destruct "destruct on a Rel: called by set in interp_tbl" op in
         t.(index) <- mk_Tval hval.tparams hval.tres hval.op_val in
       Hashtbl.iter set reify.tbl;
-      CoqInterface.mkArray (tval, t)
+      CoqTerms.mkArray (tval, t)
 
     let to_list reify =
       let set _ op acc =
@@ -1435,7 +1435,7 @@ module Atom =
 
     let interp_tbl reify =
       let t = to_array reify (Lazy.force dft_atom) a_to_coq in
-      CoqInterface.mkArray (Lazy.force catom, t)
+      CoqTerms.mkArray (Lazy.force catom, t)
 
 
     (** Producing a Coq term corresponding to the interpretation of an atom *)
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index c610129..923874e 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -156,7 +156,7 @@ let interp_tbl reify =
       | _ -> Some bt
   in
   Hashtbl.filter_map_inplace set reify.tbl;
-  CoqInterface.mkArray (Lazy.force ctyp_compdec, t)
+  CoqTerms.mkArray (Lazy.force ctyp_compdec, t)
 
 
 let to_list reify =
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index fba59e1..c8f02ba 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -18,65 +18,57 @@ open SmtTrace
 open SmtCertif
 
 
-let euf_checker_modules = [ ["SMTCoq";"Trace";"Euf_Checker"] ]
-let certif_ops args = CoqTerms.make_certif_ops euf_checker_modules args
-let cCertif = gen_constant euf_checker_modules "Certif"
-let ccertif = gen_constant euf_checker_modules "certif"
-let cchecker = gen_constant euf_checker_modules "checker"
-let cchecker_correct = gen_constant euf_checker_modules "checker_correct"
-let cchecker_b_correct =
-  gen_constant euf_checker_modules "checker_b_correct"
-let cchecker_b = gen_constant euf_checker_modules "checker_b"
-let cchecker_eq_correct =
-  gen_constant euf_checker_modules "checker_eq_correct"
-let cchecker_eq = gen_constant euf_checker_modules "checker_eq"
-(* let csetup_checker_step_debug =
- *   gen_constant euf_checker_modules "setup_checker_step_debug" *)
-(* let cchecker_step_debug = gen_constant euf_checker_modules "checker_step_debug" *)
-(* let cstep = gen_constant euf_checker_modules "step" *)
-let cchecker_debug = gen_constant euf_checker_modules "checker_debug"
-
-let cname_step = gen_constant euf_checker_modules "name_step"
-
-let cName_Res = gen_constant euf_checker_modules "Name_Res"
-let cName_Weaken= gen_constant euf_checker_modules "Name_Weaken"
-let cName_ImmFlatten= gen_constant euf_checker_modules "Name_ImmFlatten"
-let cName_CTrue= gen_constant euf_checker_modules "Name_CTrue"
-let cName_CFalse = gen_constant euf_checker_modules "Name_CFalse"
-let cName_BuildDef= gen_constant euf_checker_modules "Name_BuildDef"
-let cName_BuildDef2= gen_constant euf_checker_modules "Name_BuildDef2"
-let cName_BuildProj = gen_constant euf_checker_modules "Name_BuildProj"
-let cName_ImmBuildDef= gen_constant euf_checker_modules "Name_ImmBuildDef"
-let cName_ImmBuildDef2= gen_constant euf_checker_modules "Name_ImmBuildDef2"
-let cName_ImmBuildProj = gen_constant euf_checker_modules "Name_ImmBuildProj"
-let cName_EqTr = gen_constant euf_checker_modules "Name_EqTr"
-let cName_EqCgr = gen_constant euf_checker_modules "Name_EqCgr"
-let cName_EqCgrP= gen_constant euf_checker_modules "Name_EqCgrP"
-let cName_LiaMicromega = gen_constant euf_checker_modules "Name_LiaMicromega"
-let cName_LiaDiseq= gen_constant euf_checker_modules "Name_LiaDiseq"
-let cName_SplArith= gen_constant euf_checker_modules "Name_SplArith"
-let cName_SplDistinctElim = gen_constant euf_checker_modules "Name_SplDistinctElim"
-let cName_BBVar= gen_constant euf_checker_modules "Name_BBVar"
-let cName_BBConst= gen_constant euf_checker_modules "Name_BBConst"
-let cName_BBOp= gen_constant euf_checker_modules "Name_BBOp"
-let cName_BBNot= gen_constant euf_checker_modules "Name_BBNot"
-let cName_BBNeg= gen_constant euf_checker_modules "Name_BBNeg"
-let cName_BBAdd= gen_constant euf_checker_modules "Name_BBAdd"
-let cName_BBConcat= gen_constant euf_checker_modules "Name_BBConcat"
-let cName_BBMul= gen_constant euf_checker_modules "Name_BBMul"
-let cName_BBUlt= gen_constant euf_checker_modules "Name_BBUlt"
-let cName_BBSlt= gen_constant euf_checker_modules "Name_BBSlt"
-let cName_BBEq= gen_constant euf_checker_modules "Name_BBEq"
-let cName_BBDiseq= gen_constant euf_checker_modules "Name_BBDiseq"
-let cName_BBExtract= gen_constant euf_checker_modules "Name_BBExtract"
-let cName_BBZextend= gen_constant euf_checker_modules "Name_BBZextend"
-let cName_BBSextend= gen_constant euf_checker_modules "Name_BBSextend"
-let cName_BBShl= gen_constant euf_checker_modules "Name_BBShl"
-let cName_BBShr= gen_constant euf_checker_modules "Name_BBShr"
-let cName_RowEq= gen_constant euf_checker_modules "Name_RowEq"
-let cName_RowNeq= gen_constant euf_checker_modules "Name_RowNeq"
-let cName_Ext= gen_constant euf_checker_modules "Name_Ext"
-let cName_Hole= gen_constant euf_checker_modules "Name_Hole"
+let certif_ops = CoqTerms.ceuf_checker_certif_ops
+let cCertif = CoqTerms.ceuf_checker_Certif
+let ccertif = CoqTerms.ceuf_checker_certif
+let cchecker = CoqTerms.ceuf_checker_checker
+let cchecker_correct = CoqTerms.ceuf_checker_checker_correct
+let cchecker_b_correct = CoqTerms.ceuf_checker_checker_b_correct
+let cchecker_b = CoqTerms.ceuf_checker_checker_b
+let cchecker_eq_correct = CoqTerms.ceuf_checker_checker_eq_correct
+let cchecker_eq = CoqTerms.ceuf_checker_checker_eq
+let cchecker_debug = CoqTerms.ceuf_checker_checker_debug
+let cname_step = CoqTerms.ceuf_checker_name_step
+let cName_Res = CoqTerms.ceuf_checker_Name_Res
+let cName_Weaken = CoqTerms.ceuf_checker_Name_Weaken
+let cName_ImmFlatten = CoqTerms.ceuf_checker_Name_ImmFlatten
+let cName_CTrue = CoqTerms.ceuf_checker_Name_CTrue
+let cName_CFalse = CoqTerms.ceuf_checker_Name_CFalse
+let cName_BuildDef = CoqTerms.ceuf_checker_Name_BuildDef
+let cName_BuildDef2 = CoqTerms.ceuf_checker_Name_BuildDef2
+let cName_BuildProj = CoqTerms.ceuf_checker_Name_BuildProj
+let cName_ImmBuildDef = CoqTerms.ceuf_checker_Name_ImmBuildDef
+let cName_ImmBuildDef2 = CoqTerms.ceuf_checker_Name_ImmBuildDef2
+let cName_ImmBuildProj = CoqTerms.ceuf_checker_Name_ImmBuildProj
+let cName_EqTr = CoqTerms.ceuf_checker_Name_EqTr
+let cName_EqCgr = CoqTerms.ceuf_checker_Name_EqCgr
+let cName_EqCgrP = CoqTerms.ceuf_checker_Name_EqCgrP
+let cName_LiaMicromega = CoqTerms.ceuf_checker_Name_LiaMicromega
+let cName_LiaDiseq = CoqTerms.ceuf_checker_Name_LiaDiseq
+let cName_SplArith = CoqTerms.ceuf_checker_Name_SplArith
+let cName_SplDistinctElim = CoqTerms.ceuf_checker_Name_SplDistinctElim
+let cName_BBVar = CoqTerms.ceuf_checker_Name_BBVar
+let cName_BBConst = CoqTerms.ceuf_checker_Name_BBConst
+let cName_BBOp = CoqTerms.ceuf_checker_Name_BBOp
+let cName_BBNot = CoqTerms.ceuf_checker_Name_BBNot
+let cName_BBNeg = CoqTerms.ceuf_checker_Name_BBNeg
+let cName_BBAdd = CoqTerms.ceuf_checker_Name_BBAdd
+let cName_BBConcat = CoqTerms.ceuf_checker_Name_BBConcat
+let cName_BBMul = CoqTerms.ceuf_checker_Name_BBMul
+let cName_BBUlt = CoqTerms.ceuf_checker_Name_BBUlt
+let cName_BBSlt = CoqTerms.ceuf_checker_Name_BBSlt
+let cName_BBEq = CoqTerms.ceuf_checker_Name_BBEq
+let cName_BBDiseq = CoqTerms.ceuf_checker_Name_BBDiseq
+let cName_BBExtract = CoqTerms.ceuf_checker_Name_BBExtract
+let cName_BBZextend = CoqTerms.ceuf_checker_Name_BBZextend
+let cName_BBSextend = CoqTerms.ceuf_checker_Name_BBSextend
+let cName_BBShl = CoqTerms.ceuf_checker_Name_BBShl
+let cName_BBShr = CoqTerms.ceuf_checker_Name_BBShr
+let cName_RowEq = CoqTerms.ceuf_checker_Name_RowEq
+let cName_RowNeq = CoqTerms.ceuf_checker_Name_RowNeq
+let cName_Ext = CoqTerms.ceuf_checker_Name_Ext
+let cName_Hole = CoqTerms.ceuf_checker_Name_Hole
+
 
 (* Given an SMT-LIB2 file and a certif, build the corresponding objects *)
 
@@ -155,13 +147,13 @@ let parse_certif t_i t_func t_atom t_form root used_root trace (rt, ro, ra, rf,
     let res = Array.make (List.length roots + 1) (mkInt 0) in
     let i = ref 0 in
     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
-    CoqInterface.mkArray (Lazy.force cint, res) in
+    CoqTerms.mkArray (Lazy.force cint, res) in
   let used_roots =
     let l = List.length used_roots in
     let res = Array.make (l + 1) (mkInt 0) in
     let i = ref (l-1) in
     List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
-    mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.mkArray (Lazy.force cint, res)|] in
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in
   let ce3 = CoqInterface.mkUConst roots in
   let _ = CoqInterface.declare_constant root ce3 in
   let ce3' = CoqInterface.mkUConst used_roots in
@@ -217,12 +209,12 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
     let res = Array.make (l + 1) (mkInt 0) in
     let i = ref (l-1) in
     List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
-    mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.mkArray (Lazy.force cint, res)|] in
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in
   let rootsCstr =
     let res = Array.make (List.length roots + 1) (mkInt 0) in
     let i = ref 0 in
     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
-    CoqInterface.mkArray (Lazy.force cint, res) in
+    CoqTerms.mkArray (Lazy.force cint, res) in
 
   let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots t_i roots|]|] in
   let theorem_proof_cast =
@@ -294,12 +286,12 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
     let res = Array.make (l + 1) (mkInt 0) in
     let i = ref (l-1) in
     List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
-    mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.mkArray (Lazy.force cint, res)|] in
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqTerms.mkArray (Lazy.force cint, res)|] in
   let rootsCstr =
     let res = Array.make (List.length roots + 1) (mkInt 0) in
     let i = ref 0 in
     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
-    CoqInterface.mkArray (Lazy.force cint, res) in
+    CoqTerms.mkArray (Lazy.force cint, res) in
 
   let tm =
    CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
@@ -364,12 +356,12 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
     let i = ref (l-1) in
     List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
     mklApp cSome [|mklApp carray [|Lazy.force cint|];
-                   CoqInterface.mkArray (Lazy.force cint, res)|] in
+                   CoqTerms.mkArray (Lazy.force cint, res)|] in
   let rootsCstr =
     let res = Array.make (List.length roots + 1) (mkInt 0) in
     let i = ref 0 in
     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
-    CoqInterface.mkArray (Lazy.force cint, res) in
+    CoqTerms.mkArray (Lazy.force cint, res) in
 
   let tm =
    CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
@@ -492,14 +484,14 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
  *     let res = Array.make (List.length roots + 1) (mkInt 0) in
  *     let i = ref 0 in
  *     List.iter (fun j -> res.(!i) <- mkInt (Form.to_lit j); incr i) roots;
- *     CoqInterface.mkArray (Lazy.force cint, res) in
+ *     CoqTerms.mkArray (Lazy.force cint, res) in
  *   let cused_roots =
  *     let l = List.length used_roots in
  *     let res = Array.make (l + 1) (mkInt 0) in
  *     let i = ref (l-1) in
  *     List.iter (fun j -> res.(!i) <- mkInt j; decr i) used_roots;
  *     mklApp cSome [|mklApp carray [|Lazy.force cint|];
- *                    CoqInterface.mkArray (Lazy.force cint, res)|] in
+ *                    CoqTerms.mkArray (Lazy.force cint, res)|] in
  *   let ce3 = CoqInterface.mkUConst croots in
  *   let _ = CoqInterface.declare_constant root ce3 in
  *   let ce3' = CoqInterface.mkUConst cused_roots in
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 0a7d859..0a5f693 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -546,7 +546,7 @@ module Make (Atom:ATOM) =
     let args_to_coq args =
       let cargs = Array.make (Array.length args + 1) (mkInt 0) in
       Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args;
-      CoqInterface.mkArray (Lazy.force cint, cargs)
+      CoqTerms.mkArray (Lazy.force cint, cargs)
 
     let pf_to_coq = function
       | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|]
@@ -586,7 +586,7 @@ module Make (Atom:ATOM) =
 
     let interp_tbl reify =
       let (i,t) = to_array reify (Lazy.force cFtrue) pf_to_coq in
-      (mkInt i, CoqInterface.mkArray (Lazy.force cform, t))
+      (mkInt i, CoqTerms.mkArray (Lazy.force cform, t))
 
     let nvars reify = reify.count
     (* Producing a Coq term corresponding to the interpretation of a formula *)
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 7b68a26..470742a 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -383,7 +383,7 @@ let to_coq to_lit interp (cstep,
 	      l := tl
 	  | _ -> assert false
 	done;
-	mklApp cRes [|mkInt (get_pos c); CoqInterface.mkArray (Lazy.force cint, args)|]
+	mklApp cRes [|mkInt (get_pos c); CoqTerms.mkArray (Lazy.force cint, args)|]
     | Other other ->
 	begin match other with
         | Weaken (c',l') ->
@@ -412,12 +412,12 @@ let to_coq to_lit interp (cstep,
           mklApp cEqCgrP [|out_c c; out_f f1; out_f f2; res|]
 	| LiaMicromega (cl,d) ->
           let cl' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force cint; out_f f; l|]) cl (mklApp cnil [|Lazy.force cint|]) in
-          let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force CoqInterface.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force CoqInterface.micromega_coq_proofTerm|]) in
+          let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force CoqTerms.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force CoqTerms.micromega_coq_proofTerm|]) in
           mklApp cLiaMicromega [|out_c c; cl'; c'|]
         | LiaDiseq l -> mklApp cLiaDiseq [|out_c c; out_f l|]
         | SplArith (orig,res,l) ->
           let res' = out_f res in
-          let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force CoqInterface.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force CoqInterface.micromega_coq_proofTerm|]) in
+          let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force CoqTerms.micromega_coq_proofTerm; CoqInterface.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force CoqTerms.micromega_coq_proofTerm|]) in
           mklApp cSplArith [|out_c c; out_c orig; res'; l'|]
 	| SplDistinctElim (c',f) -> mklApp cSplDistinctElim [|out_c c;out_c c'; out_f f|]
         | BBVar res -> mklApp cBBVar [|out_c c; out_f res|]
@@ -483,7 +483,7 @@ let to_coq to_lit interp (cstep,
     | _ -> assert false in
   let step = Lazy.force cstep in
   let def_step =
-    mklApp cRes [|mkInt 0; CoqInterface.mkArray (Lazy.force cint, [|mkInt 0|]) |] in
+    mklApp cRes [|mkInt 0; CoqTerms.mkArray (Lazy.force cint, [|mkInt 0|]) |] in
   let r = ref confl in
   let nc = ref 0 in
   while not (isRoot !r.kind) do r := prev !r; incr nc done;
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index 1f5110b..89dd13e 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -133,7 +133,7 @@ let import_cnf_trace reloc filename first last =
 
 let make_roots first last =
   let cint = Lazy.force cint in
-  let roots = Array.make (last.id + 2) (CoqInterface.mkArray (cint, Array.make 1 (mkInt 0))) in
+  let roots = Array.make (last.id + 2) (CoqTerms.mkArray (cint, Array.make 1 (mkInt 0))) in
   let mk_elem l =
     let x = match Form.pform l with
     | Fatom x -> x + 2
@@ -144,15 +144,15 @@ let make_roots first last =
     let root = Array.of_list (get_val !r) in
     let croot = Array.make (Array.length root + 1) (mkInt 0) in
     Array.iteri (fun i l -> croot.(i) <- mk_elem l) root;
-    roots.(!r.id) <- CoqInterface.mkArray (cint, croot);
+    roots.(!r.id) <- CoqTerms.mkArray (cint, croot);
     r := next !r
   done;
   let root = Array.of_list (get_val !r) in
   let croot = Array.make (Array.length root + 1) (mkInt 0) in
   Array.iteri (fun i l -> croot.(i) <- mk_elem l) root;
-  roots.(!r.id) <- CoqInterface.mkArray (cint, croot);
+  roots.(!r.id) <- CoqTerms.mkArray (cint, croot);
 
-  CoqInterface.mkArray (mklApp carray [|cint|], roots)
+  CoqTerms.mkArray (mklApp carray [|cint|], roots)
 
 let interp_roots first last =
   let tbl = Hashtbl.create 17 in
@@ -185,10 +185,8 @@ let interp_roots first last =
   end;
   !res
 
-let sat_checker_modules = [ ["SMTCoq";"Trace";"Sat_Checker"] ]
-
-let certif_ops = CoqTerms.make_certif_ops sat_checker_modules None
-let cCertif = gen_constant sat_checker_modules "Certif"
+let certif_ops = CoqTerms.csat_checker_certif_ops
+let cCertif = CoqTerms.csat_checker_Certif
 
 let parse_certif dimacs trace fdimacs ftrace =
   SmtTrace.clear ();
@@ -205,10 +203,10 @@ let parse_certif dimacs trace fdimacs ftrace =
   let _ = CoqInterface.declare_constant trace ce2 in
   ()
 
-let cdimacs = gen_constant sat_checker_modules "dimacs"
-let ccertif = gen_constant sat_checker_modules "certif"
-let ctheorem_checker = gen_constant sat_checker_modules "theorem_checker"
-let cchecker = gen_constant sat_checker_modules "checker"
+let cdimacs = CoqTerms.csat_checker_dimacs
+let ccertif = CoqTerms.csat_checker_certif
+let ctheorem_checker = CoqTerms.csat_checker_theorem_checker
+let cchecker = CoqTerms.csat_checker_checker
 
 let theorems interp name fdimacs ftrace =
   SmtTrace.clear ();
@@ -251,7 +249,7 @@ let theorems interp name fdimacs ftrace =
 
 let theorem = theorems (fun _ -> interp_roots)
 let theorem_abs =
-  theorems (fun d _ _ -> mklApp cvalid_sat_checker [|mklApp cinterp_var_sat_checker [|CoqInterface.mkRel 1(*v*)|]; d|])
+  theorems (fun d _ _ -> mklApp csat_checker_valid [|mklApp csat_checker_interp_var [|CoqInterface.mkRel 1(*v*)|]; d|])
 
 
 let checker fdimacs ftrace =
@@ -345,17 +343,13 @@ let call_zchaff nvars root =
 
 (* Build the problem that it may be understoof by zchaff *)
 
-let cnf_checker_modules = [ ["SMTCoq";"Trace";"Cnf_Checker"] ]
-
-let certif_ops = CoqTerms.make_certif_ops cnf_checker_modules None
-let ccertif = gen_constant cnf_checker_modules "certif"
-let cCertif = gen_constant cnf_checker_modules "Certif"
-let cchecker_b_correct =
-  gen_constant cnf_checker_modules "checker_b_correct"
-let cchecker_b = gen_constant cnf_checker_modules "checker_b"
-let cchecker_eq_correct =
-  gen_constant cnf_checker_modules "checker_eq_correct"
-let cchecker_eq = gen_constant cnf_checker_modules "checker_eq"
+let certif_ops = CoqTerms.ccnf_checker_certif_ops
+let ccertif = CoqTerms.ccnf_checker_certif
+let cCertif = CoqTerms.ccnf_checker_Certif
+let cchecker_b_correct = CoqTerms.ccnf_checker_checker_b_correct
+let cchecker_b = CoqTerms.ccnf_checker_checker_b
+let cchecker_eq_correct = CoqTerms.ccnf_checker_checker_eq_correct
+let cchecker_eq = CoqTerms.ccnf_checker_checker_eq
 
 let build_body reify_atom reify_form l b (max_id, confl) vm_cast =
   let ntvar = CoqInterface.mkName "t_var" in