V8.7 (#36)

Port SMTCoq to Coq-8.7

9 files changed, 159 insertions, 163 deletions

diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index 76f213b..895d217 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -12,8 +12,9 @@
 
 open Coqlib
 
-let gen_constant modules constant =
-  lazy (gen_constant_in_modules "SMT" modules constant)
+
+let gen_constant = Structures.gen_constant
+
 
 (* Int63 *)
 let cint = Structures.cint
@@ -65,7 +66,7 @@ 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 cZeqbsym = gen_constant z_modules "eqb_sym" *)
 
 (* Booleans *)
 let bool_modules = [["Coq";"Bool";"Bool"]]
@@ -100,12 +101,12 @@ let cprod = gen_constant init_modules "prod"
 
 (* Dependent pairs *)
 let csigT = gen_constant init_modules "sigT"
-let cprojT1 = gen_constant init_modules "projT1"
-let cprojT2 = gen_constant init_modules "projT2"
-let cprojT3 = gen_constant init_modules "projT3"
+(* let cprojT1 = gen_constant init_modules "projT1" *)
+(* let cprojT2 = gen_constant init_modules "projT2" *)
+(* let cprojT3 = gen_constant init_modules "projT3" *)
 
-let csigT2 = gen_constant init_modules "sigT2"
-let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2"
+(* let csigT2 = gen_constant init_modules "sigT2" *)
+(* let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2" *)
 
 (* Logical Operators *)
 let cnot = gen_constant init_modules "not"
@@ -118,7 +119,7 @@ let cand = gen_constant init_modules "and"
 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 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"
@@ -147,8 +148,8 @@ let cdiff = gen_constant array_modules "diff"
 let cequalarray = gen_constant array_modules "FArray.equal"
 
 (* OrderedType *)
-let cOrderedTypeCompare =
-  gen_constant [["Coq";"Structures";"OrderedType"]] "Compare"
+(* let cOrderedTypeCompare =
+ *   gen_constant [["Coq";"Structures";"OrderedType"]] "Compare" *)
 
 (* SMT_terms *)
 let smt_modules = [ ["SMTCoq";"Misc"];
@@ -172,7 +173,7 @@ 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 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"
@@ -180,14 +181,14 @@ 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 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 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"
@@ -340,7 +341,7 @@ let mkN = function
   | i -> SmtMisc.mklApp cNpos [|mkPositive i|]
 
 (* Compute a Boolean *)
-let rec mkBool = function
+let mkBool = function
   | true -> Lazy.force ctrue
   | false -> Lazy.force cfalse
 
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index b21bef8..9aeddac 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -259,4 +259,5 @@ val mk_bool : Term.constr -> bool
 val mk_bool_list : Term.constr -> bool list
 val mk_nat : Term.constr -> int
 val mk_N : Term.constr -> int
+val mk_Z : Term.constr -> int
 val mk_bvsize : Term.constr -> int
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
index b5fe759..4ecfae3 100644
--- a/src/trace/satAtom.mli
+++ b/src/trace/satAtom.mli
@@ -21,7 +21,6 @@ module Atom : sig
   val to_smt : Format.formatter -> t -> unit
   val logic : t -> SmtMisc.logic
 
-  val is_bool_type : t -> bool
   type reify_tbl = {
       mutable count : int;
       tbl : (Term.constr, t) Hashtbl.t;
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index fd9f2bd..330884b 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -12,9 +12,6 @@
 
 open SmtMisc
 open CoqTerms
-open Entries
-open Declare
-open Decl_kinds
 open SmtBtype
 
 
@@ -229,8 +226,8 @@ module Op =
       | BO_diffarray (ti, te) -> (TFArray (ti, te), TFArray (ti, te))
 
 
-    let interp_ieq t_i t =
-      mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|]
+    (* let interp_ieq t_i t =
+     *   mklApp cinterp_eqb [|t_i ; SmtBtype.to_coq t|] *)
 
  (*   let veval_t te =
       let env = Global.env () in
@@ -246,30 +243,30 @@ module Op =
 
     let interp_eqarray t_i ti te =
       mklApp cequalarray
-        SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
-                SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
-                SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
-                SmtBtype.inh_interp t_i te |]
+        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+          SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+          SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
+          SmtBtype.inh_interp t_i te |]
 
     let interp_select t_i ti te =
       mklApp cselect
-        SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
-                SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
-                SmtBtype.inh_interp t_i te|]
+        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+          SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+          SmtBtype.inh_interp t_i te|]
 
     let interp_diff t_i ti te =
       mklApp cdiff
-        SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
-                SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
-                SmtBtype.dec_interp t_i te; SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
-                SmtBtype.inh_interp t_i ti; SmtBtype.inh_interp t_i te |]
+        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+          SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+          SmtBtype.dec_interp t_i te; SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te;
+          SmtBtype.inh_interp t_i ti; SmtBtype.inh_interp t_i te |]
 
 
     let interp_store t_i ti te =
       mklApp cstore
-        SmtBtype.[|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
-                SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
-                SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; SmtBtype.inh_interp t_i te |]
+        [|SmtBtype.interp t_i ti; SmtBtype.interp t_i te;
+          SmtBtype.dec_interp t_i ti; SmtBtype.ord_interp t_i ti; SmtBtype.comp_interp t_i ti;
+          SmtBtype.ord_interp t_i te; SmtBtype.comp_interp t_i te; SmtBtype.inh_interp t_i te |]
 
 
     let interp_eq t_i = function
@@ -1022,7 +1019,7 @@ module Atom =
           else CCunknown_deps (gobble_of_coq_cst cc)
         with Not_found -> CCunknown
       in
-      let rec mk_hatom h =
+      let rec mk_hatom (h : Term.constr) =
         let c, args = Term.decompose_app h in
 	match get_cst c with
         | CCxH -> mk_cop CCxH args
@@ -1064,9 +1061,9 @@ module Atom =
         | CCselect -> mk_bop_select args
         | CCdiff -> mk_bop_diff args
         | CCstore -> mk_top_store args
-	| CCunknown -> mk_unknown c args (Retyping.get_type_of env sigma h)
+	| CCunknown -> mk_unknown c args (Structures.retyping_get_type_of env sigma h)
         | CCunknown_deps gobble ->
-          mk_unknown_deps c args (Retyping.get_type_of env sigma h) gobble
+          mk_unknown_deps c args (Structures.retyping_get_type_of env sigma h) gobble
 
 
       and mk_cop op args = match op, args with
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index 0ebb893..119c046 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -119,8 +119,8 @@ let to_list reify =
 let make_t_i rt = interp_tbl rt
 
 
-let interp_t t_i t =
-  mklApp cinterp_t [|t_i ; to_coq t|]
+(* let interp_t t_i t =
+ *   mklApp cinterp_t [|t_i ; to_coq t|] *)
 
 let dec_interp t_i t =
   mklApp cdec_interp [|t_i ; to_coq t|]
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index b1468e4..6ce6997 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -10,8 +10,6 @@
 (**************************************************************************)
 
 
-open SmtForm
-
 type used = int
 
 type clause_id  = int
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 43365ef..1a990f1 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -34,10 +34,10 @@ 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 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"
@@ -315,7 +315,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
    Term.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
    mklApp cchecker [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*); v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in
 
-  let res = Vnorm.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
+  let res = Structures.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
   Format.eprintf "     = %s\n     : bool@."
     (if Term.eq_constr res (Lazy.force CoqTerms.ctrue) then
         "true" else "false")
@@ -389,7 +389,7 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
    mklApp cchecker_debug [|v 7 (*t_i*); v 6 (*t_func*); v 5 (*t_atom*);
        v 4 (*t_form*); v 1 (*d*); v 2 (*used_roots*); v 3 (*c*)|]))))))) in
 
-  let res = Vnorm.cbv_vm (Global.env ()) tm
+  let res = Structures.cbv_vm (Global.env ()) tm
       (mklApp coption
          [|mklApp cprod
              [|Lazy.force cnat; Lazy.force cname_step|]|]) in
@@ -453,117 +453,117 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
 
 
 
-let rec of_coq_list cl =
-  match Term.decompose_app cl with
-  | c, _ when Term.eq_constr c (Lazy.force cnil) -> []
-  | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) ->
-    x :: of_coq_list cr
-  | _ -> assert false
-
-
-let checker_debug_step t_i t_func t_atom t_form root used_root trace
-    (rt, ro, ra, rf, roots, max_id, confl) =
-
-  let t_i' = make_t_i rt in
-  let ce5 = Structures.mkUConst t_i' in
-  let ct_i = Term.mkConst (declare_constant t_i
-                             (DefinitionEntry ce5, IsDefinition Definition)) in
-
-  let t_func' = make_t_func ro ct_i in
-  let ce6 = Structures.mkUConst t_func' in
-  let ct_func =
-    Term.mkConst (declare_constant t_func
-                    (DefinitionEntry ce6, IsDefinition Definition)) in
-
-  let t_atom' = Atom.interp_tbl ra in
-  let ce1 = Structures.mkUConst t_atom' in
-  let ct_atom =
-    Term.mkConst (declare_constant t_atom
-                    (DefinitionEntry ce1, IsDefinition Definition)) in
-
-  let t_form' = snd (Form.interp_tbl rf) in
-  let ce2 = Structures.mkUConst t_form' in
-  let ct_form =
-    Term.mkConst (declare_constant t_form
-                    (DefinitionEntry ce2, IsDefinition Definition)) in
-
-  let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
-      (interp_conseq_uf ct_i)
-      (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
-  List.iter (fun (v,ty) ->
-    let _ = Structures.declare_new_variable v ty in
-    print_assm ty
-  ) cuts;
-
-  let used_roots = compute_roots roots last_root in
-  let croots =
-    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;
-    Structures.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|];
-                   Structures.mkArray (Lazy.force cint, res)|] in
-  let ce3 = Structures.mkUConst croots in
-  let _ = declare_constant root
-      (DefinitionEntry ce3, IsDefinition Definition) in
-  let ce3' = Structures.mkUConst cused_roots in
-  let _ = declare_constant used_root
-      (DefinitionEntry ce3', IsDefinition Definition) in
-
-  let certif =
-    mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1);
-                     tres;mkInt (get_pos confl)|] in
-  let ce4 = Structures.mkUConst certif in
-  let _ = declare_constant trace
-      (DefinitionEntry ce4, IsDefinition Definition) in
-
-  let setup =
-   mklApp csetup_checker_step_debug
-     [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in
-
-  let setup = Vnorm.cbv_vm (Global.env ()) setup
-      (mklApp cprod
-         [|Lazy.force cState_S_t;
-           mklApp clist [|mklApp cstep
-                            [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in
-
-  let s, steps = match Term.decompose_app setup with
-    | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) ->
-      s, of_coq_list csteps
-    | _ -> assert false
-  in
-
-  let cpt = ref (List.length roots) in
-  let debug_step s step =
-    incr cpt;
-    Format.eprintf "%d@." !cpt;
-    let tm =
-      mklApp cchecker_step_debug
-        [| ct_i; ct_func; ct_atom; ct_form; s; step |] in
-
-    let res =
-      Vnorm.cbv_vm (Global.env ()) tm
-          (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in
-
-    match Term.decompose_app res with
-    | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) ->
-      if not (mk_bool cbad) then s
-      else Structures.error ("Step number " ^ string_of_int !cpt ^
-                             " (" ^ string_coq_constr
-                               (fst (Term.decompose_app step)) ^ ")" ^
-                             " of the certificate likely failed." )
-    | _ -> assert false
-  in
-
-  List.fold_left debug_step s steps |> ignore;
-
-  Structures.error ("Debug checker is only meant to be used for certificates \
-                     that fail to be checked by SMTCoq.")
+(* let rec of_coq_list cl =
+ *   match Term.decompose_app cl with
+ *   | c, _ when Term.eq_constr c (Lazy.force cnil) -> []
+ *   | c, [_; x; cr] when Term.eq_constr c (Lazy.force ccons) ->
+ *     x :: of_coq_list cr
+ *   | _ -> assert false *)
+
+
+(* let checker_debug_step t_i t_func t_atom t_form root used_root trace
+ *     (rt, ro, ra, rf, roots, max_id, confl) =
+ * 
+ *   let t_i' = make_t_i rt in
+ *   let ce5 = Structures.mkUConst t_i' in
+ *   let ct_i = Term.mkConst (declare_constant t_i
+ *                              (DefinitionEntry ce5, IsDefinition Definition)) in
+ * 
+ *   let t_func' = make_t_func ro ct_i in
+ *   let ce6 = Structures.mkUConst t_func' in
+ *   let ct_func =
+ *     Term.mkConst (declare_constant t_func
+ *                     (DefinitionEntry ce6, IsDefinition Definition)) in
+ * 
+ *   let t_atom' = Atom.interp_tbl ra in
+ *   let ce1 = Structures.mkUConst t_atom' in
+ *   let ct_atom =
+ *     Term.mkConst (declare_constant t_atom
+ *                     (DefinitionEntry ce1, IsDefinition Definition)) in
+ * 
+ *   let t_form' = snd (Form.interp_tbl rf) in
+ *   let ce2 = Structures.mkUConst t_form' in
+ *   let ct_form =
+ *     Term.mkConst (declare_constant t_form
+ *                     (DefinitionEntry ce2, IsDefinition Definition)) in
+ * 
+ *   let (tres, last_root, cuts) = SmtTrace.to_coq (fun i -> mkInt (Form.to_lit i))
+ *       (interp_conseq_uf ct_i)
+ *       (certif_ops (Some [|ct_i; ct_func; ct_atom; ct_form|])) confl None in
+ *   List.iter (fun (v,ty) ->
+ *     let _ = Structures.declare_new_variable v ty in
+ *     print_assm ty
+ *   ) cuts;
+ * 
+ *   let used_roots = compute_roots roots last_root in
+ *   let croots =
+ *     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;
+ *     Structures.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|];
+ *                    Structures.mkArray (Lazy.force cint, res)|] in
+ *   let ce3 = Structures.mkUConst croots in
+ *   let _ = declare_constant root
+ *       (DefinitionEntry ce3, IsDefinition Definition) in
+ *   let ce3' = Structures.mkUConst cused_roots in
+ *   let _ = declare_constant used_root
+ *       (DefinitionEntry ce3', IsDefinition Definition) in
+ * 
+ *   let certif =
+ *     mklApp cCertif [|ct_i; ct_func; ct_atom; ct_form; mkInt (max_id + 1);
+ *                      tres;mkInt (get_pos confl)|] in
+ *   let ce4 = Structures.mkUConst certif in
+ *   let _ = declare_constant trace
+ *       (DefinitionEntry ce4, IsDefinition Definition) in
+ * 
+ *   let setup =
+ *    mklApp csetup_checker_step_debug
+ *      [| ct_i; ct_func; ct_atom; ct_form; croots; cused_roots; certif |] in
+ * 
+ *   let setup = Structures.cbv_vm (Global.env ()) setup
+ *       (mklApp cprod
+ *          [|Lazy.force cState_S_t;
+ *            mklApp clist [|mklApp cstep
+ *                             [|ct_i; ct_func; ct_atom; ct_form|]|]|]) in
+ * 
+ *   let s, steps = match Term.decompose_app setup with
+ *     | c, [_; _; s; csteps] when Term.eq_constr c (Lazy.force cpair) ->
+ *       s, of_coq_list csteps
+ *     | _ -> assert false
+ *   in
+ * 
+ *   let cpt = ref (List.length roots) in
+ *   let debug_step s step =
+ *     incr cpt;
+ *     Format.eprintf "%d@." !cpt;
+ *     let tm =
+ *       mklApp cchecker_step_debug
+ *         [| ct_i; ct_func; ct_atom; ct_form; s; step |] in
+ * 
+ *     let res =
+ *       Structures.cbv_vm (Global.env ()) tm
+ *           (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in
+ * 
+ *     match Term.decompose_app res with
+ *     | c, [_; _; s; cbad] when Term.eq_constr c (Lazy.force cpair) ->
+ *       if not (mk_bool cbad) then s
+ *       else Structures.error ("Step number " ^ string_of_int !cpt ^
+ *                              " (" ^ string_coq_constr
+ *                                (fst (Term.decompose_app step)) ^ ")" ^
+ *                              " of the certificate likely failed." )
+ *     | _ -> assert false
+ *   in
+ * 
+ *   List.fold_left debug_step s steps |> ignore;
+ * 
+ *   Structures.error ("Debug checker is only meant to be used for certificates \
+ *                      that fail to be checked by SMTCoq.") *)
 
 
 
@@ -725,7 +725,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra' rf' vm_cast lcpl lcepl
 
   let tlcepl = List.map (Structures.interp_constr env sigma) lcepl in
   let lcpl = lcpl @ tlcepl in
-  let lcl = List.map (Retyping.get_type_of env sigma) lcpl in
+  let lcl = List.map (Structures.retyping_get_type_of env sigma) lcpl in
 
   let lsmt  = List.map (of_coq_lemma rt ro ra' rf' env sigma solver_logic) lcl in
   let l_pl_ls = List.combine (List.combine lcl lcpl) lsmt in
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 4138e7c..ad6a5a4 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -618,7 +618,7 @@ module Make (Atom:ATOM) =
 		             mklApp cifb (Array.map interp_form args)
 		          | Fnot2 n ->
 		             (let r = ref (interp_form args.(0)) in
-		              for i = 1 to n do
+		              for _ = 1 to n do
                                 r := mklApp cnegb [|!r|]
                               done;
                               !r)
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index b410f88..a9855a2 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -409,12 +409,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 Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm; Structures.Micromega_plugin_Coq_micromega.dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm|]) in
+          let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.micromega_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Structures.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 Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm; Structures.Micromega_plugin_Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Structures.Micromega_plugin_Coq_micromega.M.coq_proofTerm|]) in
+          let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Structures.micromega_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Structures.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|]