From e12110637730d067c216abcc86185b761189b342 Mon Sep 17 00:00:00 2001
From: vblot <24938579+vblot@users.noreply.github.com>
Date: Fri, 28 May 2021 18:29:37 +0200
Subject: getting rid of native-coq (#95)

---
 src/trace/smtCommands.ml | 432 +++++++++++++++++++++++------------------------
 1 file changed, 216 insertions(+), 216 deletions(-)

(limited to 'src/trace/smtCommands.ml')

diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index fa2a56b..e655a9d 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -115,7 +115,7 @@ let interp_conseq_uf t_i (prem, concl) =
   let tf = Hashtbl.create 17 in
   let rec interp = function
     | [] -> mklApp cis_true [|interp_uf t_i ta tf concl|]
-    | c::prem -> Structures.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
+    | c::prem -> CoqInterface.mkArrow (mklApp cis_true [|interp_uf t_i ta tf c|]) (interp prem) in
   interp prem
 
 
@@ -127,26 +127,26 @@ let print_assm ty =
 let parse_certif 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 = Structures.mkConst (Structures.declare_constant t_i ce5) in
+  let ce5 = CoqInterface.mkUConst t_i' in
+  let ct_i = CoqInterface.mkConst (CoqInterface.declare_constant t_i ce5) in
 
   let t_func' = make_t_func ro ct_i in
-  let ce6 = Structures.mkUConst t_func' in
-  let ct_func = Structures.mkConst (Structures.declare_constant t_func ce6) in
+  let ce6 = CoqInterface.mkUConst t_func' in
+  let ct_func = CoqInterface.mkConst (CoqInterface.declare_constant t_func ce6) in
 
   let t_atom' = Atom.interp_tbl ra in
-  let ce1 = Structures.mkUConst t_atom' in
-  let ct_atom = Structures.mkConst (Structures.declare_constant t_atom ce1) in
+  let ce1 = CoqInterface.mkUConst t_atom' in
+  let ct_atom = CoqInterface.mkConst (CoqInterface.declare_constant t_atom ce1) in
 
   let t_form' = snd (Form.interp_tbl rf) in
-  let ce2 = Structures.mkUConst t_form' in
-  let ct_form = Structures.mkConst (Structures.declare_constant t_form ce2) in
+  let ce2 = CoqInterface.mkUConst t_form' in
+  let ct_form = CoqInterface.mkConst (CoqInterface.declare_constant t_form ce2) in
 
   (* EMPTY LEMMA LIST *)
   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
+    let _ = CoqInterface.declare_new_variable v ty in
     print_assm ty
   ) cuts;
 
@@ -155,22 +155,22 @@ 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;
-    Structures.mkArray (Lazy.force cint, res) in
+    CoqInterface.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|]; Structures.mkArray (Lazy.force cint, res)|] in
-  let ce3 = Structures.mkUConst roots in
-  let _ = Structures.declare_constant root ce3 in
-  let ce3' = Structures.mkUConst used_roots in
-  let _ = Structures.declare_constant used_root ce3' in
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.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
+  let _ = CoqInterface.declare_constant used_root ce3' 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 _ = Structures.declare_constant trace ce4 in
+  let ce4 = CoqInterface.mkUConst certif in
+  let _ = CoqInterface.declare_constant trace ce4 in
 
   ()
 
@@ -184,15 +184,15 @@ let interp_roots t_i roots =
     | f::roots -> List.fold_left (fun acc f -> mklApp candb [|acc; interp f|]) (interp f) roots
 
 let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
-  let nti = Structures.mkName "t_i" in
-  let ntfunc = Structures.mkName "t_func" in
-  let ntatom = Structures.mkName "t_atom" in
-  let ntform = Structures.mkName "t_form" in
-  let nc = Structures.mkName "c" in
-  let nused_roots = Structures.mkName "used_roots" in
-  let nd = Structures.mkName "d" in
+  let nti = CoqInterface.mkName "t_i" in
+  let ntfunc = CoqInterface.mkName "t_func" in
+  let ntatom = CoqInterface.mkName "t_atom" in
+  let ntform = CoqInterface.mkName "t_form" in
+  let nc = CoqInterface.mkName "c" in
+  let nused_roots = CoqInterface.mkName "used_roots" in
+  let nd = CoqInterface.mkName "d" in
 
-  let v = Structures.mkRel in
+  let v = CoqInterface.mkRel in
 
   let t_i = make_t_i rt in
   let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -204,7 +204,7 @@ let theorem name (rt, ro, ra, rf, roots, max_id, confl) =
       (interp_conseq_uf t_i)
       (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
   List.iter (fun (v,ty) ->
-    let _ = Structures.declare_new_variable v ty in
+    let _ = CoqInterface.declare_new_variable v ty in
     print_assm ty
   ) cuts;
 
@@ -217,59 +217,59 @@ 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|]; Structures.mkArray (Lazy.force cint, res)|] in
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.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;
-    Structures.mkArray (Lazy.force cint, res) in
+    CoqInterface.mkArray (Lazy.force cint, res) in
 
   let theorem_concl = mklApp cnot [|mklApp cis_true [|interp_roots t_i roots|]|] in
   let theorem_proof_cast =
-    Structures.mkCast (
-        Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-        Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
-        Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-        Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-        Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
-        Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
-        Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+    CoqInterface.mkCast (
+        CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+        CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
+        CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+        CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+        CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+        CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+        CoqInterface.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
         mklApp cchecker_correct
                [|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*);
 	         vm_cast_true_no_check
 	           (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*)|])|]))))))),
-        Structures.vmcast,
+        CoqInterface.vmcast,
         theorem_concl)
   in
   let theorem_proof_nocast =
-        Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-        Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
-        Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-        Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-        Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
-        Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
-        Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+        CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+        CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
+        CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+        CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+        CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+        CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+        CoqInterface.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
         mklApp cchecker_correct
                [|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 ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_concl in
-  let _ = Structures.declare_constant name ce in
+  let ce = CoqInterface.mkTConst theorem_proof_cast theorem_proof_nocast theorem_concl in
+  let _ = CoqInterface.declare_constant name ce in
   ()
 
 
 (* Given an SMT-LIB2 file and a certif, call the checker *)
 
 let checker (rt, ro, ra, rf, roots, max_id, confl) =
-  let nti = Structures.mkName "t_i" in
-  let ntfunc = Structures.mkName "t_func" in
-  let ntatom = Structures.mkName "t_atom" in
-  let ntform = Structures.mkName "t_form" in
-  let nc = Structures.mkName "c" in
-  let nused_roots = Structures.mkName "used_roots" in
-  let nd = Structures.mkName "d" in
+  let nti = CoqInterface.mkName "t_i" in
+  let ntfunc = CoqInterface.mkName "t_func" in
+  let ntatom = CoqInterface.mkName "t_atom" in
+  let ntform = CoqInterface.mkName "t_form" in
+  let nc = CoqInterface.mkName "c" in
+  let nused_roots = CoqInterface.mkName "used_roots" in
+  let nd = CoqInterface.mkName "d" in
 
-  let v = Structures.mkRel in
+  let v = CoqInterface.mkRel in
 
   let t_i = make_t_i rt in
   let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -281,7 +281,7 @@ let checker (rt, ro, ra, rf, roots, max_id, confl) =
       (interp_conseq_uf t_i)
       (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*); v 2(*t_atom*); v 1(* t_form *)|])) confl None in
   List.iter (fun (v,ty) ->
-    let _ = Structures.declare_new_variable v ty in
+    let _ = CoqInterface.declare_new_variable v ty in
     print_assm ty
   ) cuts;
 
@@ -294,26 +294,26 @@ 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|]; Structures.mkArray (Lazy.force cint, res)|] in
+    mklApp cSome [|mklApp carray [|Lazy.force cint|]; CoqInterface.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;
-    Structures.mkArray (Lazy.force cint, res) in
+    CoqInterface.mkArray (Lazy.force cint, res) in
 
   let tm =
-   Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-   Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
-   Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-   Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-   Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
-   Structures.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
-   Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+   CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+   CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
+   CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+   CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+   CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
+   CoqInterface.mkLetIn (nused_roots, used_rootsCstr, mklApp coption [|mklApp carray [|Lazy.force cint|]|],
+   CoqInterface.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 = Structures.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
+  let res = CoqInterface.cbv_vm (Global.env ()) tm (Lazy.force CoqTerms.cbool) in
   Format.eprintf "     = %s\n     : bool@."
-    (if Structures.eq_constr res (Lazy.force CoqTerms.ctrue) then
+    (if CoqInterface.eq_constr res (Lazy.force CoqTerms.ctrue) then
         "true" else "false")
 
 let count_used confl =
@@ -329,15 +329,15 @@ let count_used confl =
 
 
 let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
-  let nti = Structures.mkName "t_i" in
-  let ntfunc = Structures.mkName "t_func" in
-  let ntatom = Structures.mkName "t_atom" in
-  let ntform = Structures.mkName "t_form" in
-  let nc = Structures.mkName "c" in
-  let nused_roots = Structures.mkName "used_roots" in
-  let nd = Structures.mkName "d" in
+  let nti = CoqInterface.mkName "t_i" in
+  let ntfunc = CoqInterface.mkName "t_func" in
+  let ntatom = CoqInterface.mkName "t_atom" in
+  let ntform = CoqInterface.mkName "t_form" in
+  let nc = CoqInterface.mkName "c" in
+  let nused_roots = CoqInterface.mkName "used_roots" in
+  let nd = CoqInterface.mkName "d" in
 
-  let v = Structures.mkRel in
+  let v = CoqInterface.mkRel in
 
   let t_i = make_t_i rt in
   let t_func = make_t_func ro (v 1 (*t_i*)) in
@@ -349,7 +349,7 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
       (certif_ops (Some [|v 4(*t_i*); v 3(*t_func*);
                           v 2(*t_atom*); v 1(* t_form *)|])) confl None in
   List.iter (fun (v,ty) ->
-    let _ = Structures.declare_new_variable v ty in
+    let _ = CoqInterface.declare_new_variable v ty in
     print_assm ty
   ) cuts;
 
@@ -364,84 +364,84 @@ 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|];
-                   Structures.mkArray (Lazy.force cint, res)|] in
+                   CoqInterface.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;
-    Structures.mkArray (Lazy.force cint, res) in
+    CoqInterface.mkArray (Lazy.force cint, res) in
 
   let tm =
-   Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-   Structures.mkLetIn (ntfunc, t_func,
+   CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+   CoqInterface.mkLetIn (ntfunc, t_func,
                  mklApp carray [|mklApp ctval [|v 1(* t_i *)|]|],
-   Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-   Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-   Structures.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*);
+   CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+   CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+   CoqInterface.mkLetIn (nc, certif, mklApp ccertif [|v 4 (*t_i*); v 3 (*t_func*);
                                               v 2 (*t_atom*); v 1 (*t_form*)|],
-   Structures.mkLetIn (nused_roots, used_rootsCstr,
+   CoqInterface.mkLetIn (nused_roots, used_rootsCstr,
                  mklApp coption [|mklApp carray [|Lazy.force cint|]|],
-   Structures.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
+   CoqInterface.mkLetIn (nd, rootsCstr, mklApp carray [|Lazy.force cint|],
    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 = Structures.cbv_vm (Global.env ()) tm
+  let res = CoqInterface.cbv_vm (Global.env ()) tm
       (mklApp coption
          [|mklApp cprod
              [|Lazy.force cnat; Lazy.force cname_step|]|]) in
 
-  match Structures.decompose_app res with
-  | c, _ when Structures.eq_constr c (Lazy.force cNone) ->
-    Structures.error ("Debug checker is only meant to be used for certificates \
+  match CoqInterface.decompose_app res with
+  | c, _ when CoqInterface.eq_constr c (Lazy.force cNone) ->
+    CoqInterface.error ("Debug checker is only meant to be used for certificates \
                        that fail to be checked by SMTCoq.")
-  | c, [_; n] when Structures.eq_constr c (Lazy.force cSome) ->
-    (match Structures.decompose_app n with
-     | c, [_; _; cnb; cn] when Structures.eq_constr c (Lazy.force cpair) ->
-       let n = fst (Structures.decompose_app cn) in
+  | c, [_; n] when CoqInterface.eq_constr c (Lazy.force cSome) ->
+    (match CoqInterface.decompose_app n with
+     | c, [_; _; cnb; cn] when CoqInterface.eq_constr c (Lazy.force cpair) ->
+       let n = fst (CoqInterface.decompose_app cn) in
        let name =
-         if Structures.eq_constr n (Lazy.force cName_Res ) then "Res"
-         else if Structures.eq_constr n (Lazy.force cName_Weaken) then "Weaken"
-         else if Structures.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten"
-         else if Structures.eq_constr n (Lazy.force cName_CTrue) then "CTrue"
-         else if Structures.eq_constr n (Lazy.force cName_CFalse ) then "CFalse"
-         else if Structures.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef"
-         else if Structures.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2"
-         else if Structures.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj"
-         else if Structures.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef"
-         else if Structures.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2"
-         else if Structures.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj"
-         else if Structures.eq_constr n (Lazy.force cName_EqTr ) then "EqTr"
-         else if Structures.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr"
-         else if Structures.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP"
-         else if Structures.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega"
-         else if Structures.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq"
-         else if Structures.eq_constr n (Lazy.force cName_SplArith) then "SplArith"
-         else if Structures.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim"
-         else if Structures.eq_constr n (Lazy.force cName_BBVar) then "BBVar"
-         else if Structures.eq_constr n (Lazy.force cName_BBConst) then "BBConst"
-         else if Structures.eq_constr n (Lazy.force cName_BBOp) then "BBOp"
-         else if Structures.eq_constr n (Lazy.force cName_BBNot) then "BBNot"
-         else if Structures.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg"
-         else if Structures.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd"
-         else if Structures.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat"
-         else if Structures.eq_constr n (Lazy.force cName_BBMul) then "BBMul"
-         else if Structures.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt"
-         else if Structures.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt"
-         else if Structures.eq_constr n (Lazy.force cName_BBEq) then "BBEq"
-         else if Structures.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq"
-         else if Structures.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract"
-         else if Structures.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend"
-         else if Structures.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend"
-         else if Structures.eq_constr n (Lazy.force cName_BBShl) then "BBShl"
-         else if Structures.eq_constr n (Lazy.force cName_BBShr) then "BBShr"
-         else if Structures.eq_constr n (Lazy.force cName_RowEq) then "RowEq"
-         else if Structures.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq"
-         else if Structures.eq_constr n (Lazy.force cName_Ext) then "Ext"
-         else if Structures.eq_constr n (Lazy.force cName_Hole) then "Hole"
+         if CoqInterface.eq_constr n (Lazy.force cName_Res ) then "Res"
+         else if CoqInterface.eq_constr n (Lazy.force cName_Weaken) then "Weaken"
+         else if CoqInterface.eq_constr n (Lazy.force cName_ImmFlatten) then "ImmFlatten"
+         else if CoqInterface.eq_constr n (Lazy.force cName_CTrue) then "CTrue"
+         else if CoqInterface.eq_constr n (Lazy.force cName_CFalse ) then "CFalse"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BuildDef) then "BuildDef"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BuildDef2) then "BuildDef2"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BuildProj ) then "BuildProj"
+         else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildDef) then "ImmBuildDef"
+         else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildDef2) then "ImmBuildDef2"
+         else if CoqInterface.eq_constr n (Lazy.force cName_ImmBuildProj ) then "ImmBuildProj"
+         else if CoqInterface.eq_constr n (Lazy.force cName_EqTr ) then "EqTr"
+         else if CoqInterface.eq_constr n (Lazy.force cName_EqCgr ) then "EqCgr"
+         else if CoqInterface.eq_constr n (Lazy.force cName_EqCgrP) then "EqCgrP"
+         else if CoqInterface.eq_constr n (Lazy.force cName_LiaMicromega ) then "LiaMicromega"
+         else if CoqInterface.eq_constr n (Lazy.force cName_LiaDiseq) then "LiaDiseq"
+         else if CoqInterface.eq_constr n (Lazy.force cName_SplArith) then "SplArith"
+         else if CoqInterface.eq_constr n (Lazy.force cName_SplDistinctElim ) then "SplDistinctElim"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBVar) then "BBVar"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBConst) then "BBConst"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBOp) then "BBOp"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBNot) then "BBNot"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBNeg) then "BBNeg"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBAdd) then "BBAdd"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBConcat) then "BBConcat"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBMul) then "BBMul"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBUlt) then "BBUlt"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBSlt) then "BBSlt"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBEq) then "BBEq"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBDiseq) then "BBDiseq"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBExtract) then "BBExtract"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBZextend) then "BBZextend"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBSextend) then "BBSextend"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBShl) then "BBShl"
+         else if CoqInterface.eq_constr n (Lazy.force cName_BBShr) then "BBShr"
+         else if CoqInterface.eq_constr n (Lazy.force cName_RowEq) then "RowEq"
+         else if CoqInterface.eq_constr n (Lazy.force cName_RowNeq) then "RowNeq"
+         else if CoqInterface.eq_constr n (Lazy.force cName_Ext) then "Ext"
+         else if CoqInterface.eq_constr n (Lazy.force cName_Hole) then "Hole"
          else string_coq_constr n
        in
        let nb = mk_nat cnb + List.length roots + (confl.id + 1 - count_used confl) in
-       Structures.error ("Step number " ^ string_of_int nb ^
+       CoqInterface.error ("Step number " ^ string_of_int nb ^
                          " (" ^ name ^ ") of the certificate likely failed.")
      | _ -> assert false
     )
@@ -450,9 +450,9 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
 
 
 (* let rec of_coq_list cl =
- *   match Structures.decompose_app cl with
- *   | c, _ when Structures.eq_constr c (Lazy.force cnil) -> []
- *   | c, [_; x; cr] when Structures.eq_constr c (Lazy.force ccons) ->
+ *   match CoqInterface.decompose_app cl with
+ *   | c, _ when CoqInterface.eq_constr c (Lazy.force cnil) -> []
+ *   | c, [_; x; cr] when CoqInterface.eq_constr c (Lazy.force ccons) ->
  *     x :: of_coq_list cr
  *   | _ -> assert false *)
 
@@ -461,29 +461,29 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
  *     (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 = Structures.mkConst (Structures.declare_constant t_i ce5) in
+ *   let ce5 = CoqInterface.mkUConst t_i' in
+ *   let ct_i = CoqInterface.mkConst (CoqInterface.declare_constant t_i ce5) in
  * 
  *   let t_func' = make_t_func ro ct_i in
- *   let ce6 = Structures.mkUConst t_func' in
+ *   let ce6 = CoqInterface.mkUConst t_func' in
  *   let ct_func =
- *     Structures.mkConst (Structures.declare_constant t_func ce6) in
+ *     CoqInterface.mkConst (CoqInterface.declare_constant t_func ce6) in
  * 
  *   let t_atom' = Atom.interp_tbl ra in
- *   let ce1 = Structures.mkUConst t_atom' in
+ *   let ce1 = CoqInterface.mkUConst t_atom' in
  *   let ct_atom =
- *     Structures.mkConst (Structures.declare_constant t_atom ce1) in
+ *     CoqInterface.mkConst (CoqInterface.declare_constant t_atom ce1) in
  * 
  *   let t_form' = snd (Form.interp_tbl rf) in
- *   let ce2 = Structures.mkUConst t_form' in
+ *   let ce2 = CoqInterface.mkUConst t_form' in
  *   let ct_form =
- *     Structures.mkConst (Structures.declare_constant t_form ce2) in
+ *     CoqInterface.mkConst (CoqInterface.declare_constant t_form ce2) 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
+ *     let _ = CoqInterface.declare_new_variable v ty in
  *     print_assm ty
  *   ) cuts;
  * 
@@ -492,37 +492,37 @@ 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;
- *     Structures.mkArray (Lazy.force cint, res) in
+ *     CoqInterface.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 _ = Structures.declare_constant root ce3 in
- *   let ce3' = Structures.mkUConst cused_roots in
- *   let _ = Structures.declare_constant used_root ce3' in
+ *                    CoqInterface.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
+ *   let _ = CoqInterface.declare_constant used_root ce3' 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 _ = Structures.declare_constant trace ce4 in
+ *   let ce4 = CoqInterface.mkUConst certif in
+ *   let _ = CoqInterface.declare_constant trace ce4 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
+ *   let setup = CoqInterface.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 Structures.decompose_app setup with
- *     | c, [_; _; s; csteps] when Structures.eq_constr c (Lazy.force cpair) ->
+ *   let s, steps = match CoqInterface.decompose_app setup with
+ *     | c, [_; _; s; csteps] when CoqInterface.eq_constr c (Lazy.force cpair) ->
  *       s, of_coq_list csteps
  *     | _ -> assert false
  *   in
@@ -536,22 +536,22 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
  *         [| ct_i; ct_func; ct_atom; ct_form; s; step |] in
  * 
  *     let res =
- *       Structures.cbv_vm (Global.env ()) tm
+ *       CoqInterface.cbv_vm (Global.env ()) tm
  *           (mklApp cprod [|Lazy.force cState_S_t; Lazy.force cbool|]) in
  * 
- *     match Structures.decompose_app res with
- *     | c, [_; _; s; cbad] when Structures.eq_constr c (Lazy.force cpair) ->
+ *     match CoqInterface.decompose_app res with
+ *     | c, [_; _; s; cbad] when CoqInterface.eq_constr c (Lazy.force cpair) ->
  *       if not (mk_bool cbad) then s
- *       else Structures.error ("Step number " ^ string_of_int !cpt ^
+ *       else CoqInterface.error ("Step number " ^ string_of_int !cpt ^
  *                              " (" ^ string_coq_constr
- *                                (fst (Structures.decompose_app step)) ^ ")" ^
+ *                                (fst (CoqInterface.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 \
+ *   CoqInterface.error ("Debug checker is only meant to be used for certificates \
  *                      that fail to be checked by SMTCoq.") *)
 
 
@@ -559,16 +559,16 @@ let checker_debug (rt, ro, ra, rf, roots, max_id, confl) =
 (* Tactic *)
 
 let build_body rt ro ra rf l b (max_id, confl) vm_cast find =
-  let nti = Structures.mkName "t_i" in
-  let ntfunc = Structures.mkName "t_func" in
-  let ntatom = Structures.mkName "t_atom" in
-  let ntform = Structures.mkName "t_form" in
-  let nc = Structures.mkName "c" in
+  let nti = CoqInterface.mkName "t_i" in
+  let ntfunc = CoqInterface.mkName "t_func" in
+  let ntatom = CoqInterface.mkName "t_atom" in
+  let ntform = CoqInterface.mkName "t_form" in
+  let nc = CoqInterface.mkName "c" in
 
-  let v = Structures.mkRel in
+  let v = CoqInterface.mkRel in
 
   let t_i = make_t_i rt in
-  let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in
+  let t_func = CoqInterface.lift 1 (make_t_func ro (v 0 (*t_i - 1*))) in
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
   let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq
@@ -583,11 +583,11 @@ let build_body rt ro ra rf l b (max_id, confl) vm_cast find =
         mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
   let add_lets t =
-    Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-    Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
-    Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-    Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-    Structures.mkLetIn (nc, certif, mklApp ccertif
+    CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+    CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
+    CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+    CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+    CoqInterface.mkLetIn (nc, certif, mklApp ccertif
              [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
     t))))) in
 
@@ -614,16 +614,16 @@ let build_body rt ro ra rf l b (max_id, confl) vm_cast find =
 
 
 let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find =
-  let nti = Structures.mkName "t_i" in
-  let ntfunc = Structures.mkName "t_func" in
-  let ntatom = Structures.mkName "t_atom" in
-  let ntform = Structures.mkName "t_form" in
-  let nc = Structures.mkName "c" in
+  let nti = CoqInterface.mkName "t_i" in
+  let ntfunc = CoqInterface.mkName "t_func" in
+  let ntatom = CoqInterface.mkName "t_atom" in
+  let ntform = CoqInterface.mkName "t_form" in
+  let nc = CoqInterface.mkName "c" in
 
-  let v = Structures.mkRel in
+  let v = CoqInterface.mkRel in
 
   let t_i = make_t_i rt in
-  let t_func = Structures.lift 1 (make_t_func ro (v 0 (*t_i*))) in
+  let t_func = CoqInterface.lift 1 (make_t_func ro (v 0 (*t_i*))) in
   let t_atom = Atom.interp_tbl ra in
   let t_form = snd (Form.interp_tbl rf) in
   let (tres,_,cuts) = SmtTrace.to_coq Form.to_coq
@@ -633,11 +633,11 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find =
     mklApp cCertif [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*); mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
 
   let add_lets t =
-    Structures.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
-    Structures.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
-    Structures.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
-    Structures.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
-    Structures.mkLetIn (nc, certif, mklApp ccertif
+    CoqInterface.mkLetIn (nti, t_i, mklApp carray [|Lazy.force ctyp_compdec|],
+    CoqInterface.mkLetIn (ntfunc, t_func, mklApp carray [|mklApp ctval [|v 1(*t_i*)|]|],
+    CoqInterface.mkLetIn (ntatom, t_atom, mklApp carray [|Lazy.force catom|],
+    CoqInterface.mkLetIn (ntform, t_form, mklApp carray [|Lazy.force cform|],
+    CoqInterface.mkLetIn (nc, certif, mklApp ccertif
              [|v 4 (*t_i*); v 3 (*t_func*); v 2 (*t_atom*); v 1 (*t_form*)|],
     t))))) in
 
@@ -665,10 +665,10 @@ let build_body_eq rt ro ra rf l1 l2 l (max_id, confl) vm_cast find =
 
 
 let get_arguments concl =
-  let f, args = Structures.decompose_app concl in
+  let f, args = CoqInterface.decompose_app concl in
   match args with
-  | [ty;a;b] when (Structures.eq_constr f (Lazy.force ceq)) && (Structures.eq_constr ty (Lazy.force cbool)) -> a, b
-  | [a] when (Structures.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue
+  | [ty;a;b] when (CoqInterface.eq_constr f (Lazy.force ceq)) && (CoqInterface.eq_constr ty (Lazy.force cbool)) -> a, b
+  | [a] when (CoqInterface.eq_constr f (Lazy.force cis_true)) -> a, Lazy.force ctrue
   | _ -> failwith ("Verit.tactic: can only deal with equality over bool")
 
 
@@ -689,7 +689,7 @@ let gen_rel_name =
 
 let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
   let warn () =
-    Structures.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (Structures.extern_constr clemma))));
+    CoqInterface.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (CoqInterface.extern_constr clemma))));
     None
   in
 
@@ -698,16 +698,16 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
   let rel_context = List.map (fun rel -> Context.Rel.Declaration.set_name (Names.Name.mk_name (Names.Id.of_string (gen_rel_name ()))) rel) rel_context in
 
   let env_lemma = Environ.push_rel_context rel_context env in
-  let f, args = Structures.decompose_app qf_lemma in
+  let f, args = CoqInterface.decompose_app qf_lemma in
   let core_f =
-    if Structures.eq_constr f (Lazy.force cis_true) then
+    if CoqInterface.eq_constr f (Lazy.force cis_true) then
       match args with
       | [a] -> Some a
       | _ -> warn ()
-    else if Structures.eq_constr f (Lazy.force ceq) then
+    else if CoqInterface.eq_constr f (Lazy.force ceq) then
       match args with
-      | [ty; arg1; arg2] when Structures.eq_constr ty (Lazy.force cbool) &&
-                                Structures.eq_constr arg2 (Lazy.force ctrue) ->
+      | [ty; arg1; arg2] when CoqInterface.eq_constr ty (Lazy.force cbool) &&
+                                CoqInterface.eq_constr arg2 (Lazy.force ctrue) ->
          Some arg1
       | _ -> warn ()
     else warn () in
@@ -722,8 +722,8 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
       | None -> None
   in
   let forall_args =
-    let fmap r = let n, t = Structures.destruct_rel_decl r in
-                 Structures.string_of_name n, SmtBtype.of_coq rt solver_logic t in
+    let fmap r = let n, t = CoqInterface.destruct_rel_decl r in
+                 CoqInterface.string_of_name n, SmtBtype.of_coq rt solver_logic t in
     List.map fmap rel_context
   in
   match forall_args with
@@ -736,11 +736,11 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
 let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl env sigma concl =
   let a, b = get_arguments concl in
 
-  let tlcepl = List.map (Structures.interp_constr env sigma) lcepl in
+  let tlcepl = List.map (CoqInterface.interp_constr env sigma) lcepl in
   let lcpl = lcpl @ tlcepl in
 
   let create_lemma l =
-    let cl = Structures.retyping_get_type_of env sigma l in
+    let cl = CoqInterface.retyping_get_type_of env sigma l in
     match of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic cl with
       | Some smt -> Some ((cl, l), smt)
       | None -> None
@@ -748,7 +748,7 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l
   let l_pl_ls = SmtMisc.filter_map create_lemma lcpl in
   let lsmt = List.map snd l_pl_ls in
 
-  let lem_tbl : (int, Structures.constr * Structures.constr) Hashtbl.t =
+  let lem_tbl : (int, CoqInterface.constr * CoqInterface.constr) Hashtbl.t =
     Hashtbl.create 100 in
   let new_ref ((l, pl), ls) =
     Hashtbl.add lem_tbl (Form.index ls) (l, pl) in
@@ -770,11 +770,11 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l
       | _ -> failwith "unexpected form of root" in
 
   let (body_cast, body_nocast, cuts) =
-    if ((Structures.eq_constr b (Lazy.force ctrue)) ||
-        (Structures.eq_constr b (Lazy.force cfalse))) then (
+    if ((CoqInterface.eq_constr b (Lazy.force ctrue)) ||
+        (CoqInterface.eq_constr b (Lazy.force cfalse))) then (
       let l = Form.of_coq (Atom.of_coq rt ro ra solver_logic env sigma) rf a in
       let _ = Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env sigma) rf_quant a in
-      let nl = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
+      let nl = if (CoqInterface.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
       let lsmt = Form.flatten rf nl :: lsmt in
       let max_id_confl = make_proof call_solver env rt ro ra_quant rf_quant nl lsmt in
       build_body rt ro ra rf (Form.to_coq l) b max_id_confl (vm_cast env) (Some find_lemma)
@@ -793,19 +793,19 @@ let core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast l
       let cuts = (SmtBtype.get_cuts rt) @ cuts in
 
   List.fold_right (fun (eqn, eqt) tac ->
-      Structures.tclTHENLAST
-        (Structures.assert_before (Structures.name_of_id eqn) eqt)
+      CoqInterface.tclTHENLAST
+        (CoqInterface.assert_before (CoqInterface.name_of_id eqn) eqt)
         tac
     ) cuts
-    (Structures.tclTHEN
-       (Structures.set_evars_tac body_nocast)
-       (Structures.vm_cast_no_check body_cast))
+    (CoqInterface.tclTHEN
+       (CoqInterface.set_evars_tac body_nocast)
+       (CoqInterface.vm_cast_no_check body_cast))
 
 
 let tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl =
-  Structures.tclTHEN
+  CoqInterface.tclTHEN
     Tactics.intros
-    (Structures.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl))
+    (CoqInterface.mk_tactic (core_tactic call_solver solver_logic rt ro ra rf ra_quant rf_quant vm_cast lcpl lcepl))
 
 
 (**********************************************)
@@ -822,7 +822,7 @@ let string_index_of_constr env i cf =
   try
     let s = string_coq_constr cf in
     let nc = Environ.named_context env in
-    let nd = Environ.lookup_named (Structures.mkId s) env in
+    let nd = Environ.lookup_named (CoqInterface.mkId s) env in
     let cpt = ref 0 in
     (try List.iter (fun n -> incr cpt; if n == nd then raise Exit) nc
      with Exit -> ());
@@ -832,11 +832,11 @@ let string_index_of_constr env i cf =
 
 let vstring_i env i =
   let cf = SmtAtom.Atom.get_coq_term_op i in
-  if Structures.isRel cf then
-    let dbi = Structures.destRel cf in
+  if CoqInterface.isRel cf then
+    let dbi = CoqInterface.destRel cf in
     let s =
       Environ.lookup_rel dbi env
-      |> Structures.get_rel_dec_name
+      |> CoqInterface.get_rel_dec_name
       |> SmtMisc.string_of_name_def "?"
     in
     s, dbi
@@ -977,14 +977,14 @@ let model_item env rt ro ra rf =
       * let outf = Format.formatter_of_out_channel out in
       * SExpr.print outf l; pp_print_flush outf ();
       * close_out out; *)
-     Structures.error ("Could not reconstruct model")
+     CoqInterface.error ("Could not reconstruct model")
 
 
 let model env rt ro ra rf = function
   | List (Atom "model" :: l) ->
      List.fold_left (fun acc m -> match model_item env rt ro ra rf m with Fun m -> m::acc | Sort -> acc) [] l
      |> List.sort (fun ((_ ,i1), _) ((_, i2), _) -> i2 - i1)
-  | _ -> Structures.error ("No model")
+  | _ -> CoqInterface.error ("No model")
 
 
 let model_string env rt ro ra rf s =
-- 
cgit