getting rid of native-coq (#95)

60 files changed, 809 insertions, 2194 deletions

diff --git a/.gitignore b/.gitignore
index 3a518b1..15f3453 100644
--- a/.gitignore
+++ b/.gitignore
@@ -21,23 +21,10 @@ setup.log
 .lia.cache
 .nia.cache
 
-# cp targets of src/configure.sh:
-src/_CoqProject
+# targets of coq_makefile:
 src/Makefile
 src/Makefile.conf
-src/Makefile.local
-src/smtcoq_plugin.ml4
-src/versions/native/Structures.v
-src/g_smtcoq.mlg
-src/smtcoq_plugin.mlpack
-src/Tactics.v
-src/versions/standard/Int63/Int63.v
-src/versions/standard/Int63/Int63Native.v
-src/versions/standard/Int63/Int63Op.v
-src/versions/standard/Int63/Int63Axioms.v
-src/versions/standard/Int63/Int63Properties.v
-src/versions/standard/Array/PArray.v
-src/versions/standard/Structures.v
+src/g_smtcoq.ml
 
 # generated by the Makefile
 src/uninstall_me.sh
diff --git a/INSTALL.md b/INSTALL.md
index eb90daf..90b5cf5 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -81,12 +81,6 @@ You need to have OCaml version >= 4.08 and < 4.10 and Coq version 8.10.*.
 > SMTCoq. In particular this means you want a version of Coq that was compiled
 > with OCaml version >= 4.08.
 
-If you want to use SMTCoq with high performance to check large proof
-certificates, you need to use the [version of Coq with native
-data-structures](https://github.com/smtcoq/native-coq) instead of
-Coq-8.10 (warning: this allows one to use the vernacular commands but not
-the tactics).
-
 ### Install opam
 
 We recommended to install the required packages from
@@ -139,44 +133,11 @@ but you might need to install some extra packages and libraries for your system
 Compile and install SMTCoq by using the following commands in the src directory.
 
 ```bash
-./configure.sh
-make
-make install
-```
-
-## Installation with native-coq (not recommended except for high performances)
-
-> **Warning**: this installation procedure is recommended only to use
-> the vernacular commands efficiently (in particular, to check very
-> large proof certificates). It does not allow one to use the tactics.
-
-1. Download the git version of Coq with native compilation:
-```bash
-git clone https://github.com/smtcoq/native-coq.git
-```
-   and compile it by following the instructions available in the
-   repository. We recommand that you do not install it, but only compile
-   it in local:
-```bash
-./configure -local
-make
-```
-
-2. Set an environment variable COQBIN to the directory where Coq's
-   binaries are; for instance:
-```bash
-export COQBIN=/home/jdoe/native-coq/bin/
-```
-   (the final slash is mandatory).
-
-3. Compile and install SMTCoq by using the following commands in the src directory.
-```
-./configure.sh -native
+coq_makefile -f _CoqProject -o Makefile
 make
 make install
 ```
 
-
 ## Installation of the provers
 
 To use SMTCoq, we recommend installing the following two SMT solvers:
diff --git a/Makefile b/Makefile
index 5e3b013..c8be8bf 100644
--- a/Makefile
+++ b/Makefile
@@ -1,5 +1,5 @@
 all:
-	cd src && ./configure.sh && $(MAKE)
+	cd src && coq_makefile -f _CoqProject -o Makefile && $(MAKE)
 
 install: all
 	cd src && $(MAKE) install
diff --git a/ci/manifest-sources-8.11 b/ci/manifest-sources-8.11
index b93f959..795a34f 100644
--- a/ci/manifest-sources-8.11
+++ b/ci/manifest-sources-8.11
@@ -27,7 +27,7 @@ tasks:
     cd smtcoq
     git checkout coq-8.11
     cd src
-    ./configure.sh
+    coq_makefile -f _CoqProject -o Makefile
     make
     make install
     cd ../..
diff --git a/doc/sources.md b/doc/sources.md
index 55d2cec..045150d 100644
--- a/doc/sources.md
+++ b/doc/sources.md
@@ -17,14 +17,6 @@ The rest of the document describes the organization of `src`.
 SMTCoq sources are contained in this directory. A few Coq files can be found at
 top-level.
 
-### [configure.sh](../src/configure.sh)
-
-This script is meant to be run when compiling SMTCoq for the first time. It
-should also be run every time the Makefile is modified. It takes as argument an
-optional flag `-native` which, when present, will set up the sources to use the
-*native Coq* libraries. Otherwise the standard version 8.5 of Coq is used. See
-section [versions](#versions).
-
 ### [SMTCoq.v](../src/SMTCoq.v)
 
 This is the main SMTCoq entry point, it is meant to be imported by users that
@@ -142,30 +134,6 @@ This module contains miscellaneous general lemmas that are used in several
 places throughout the development of SMTCoq.
 
 
-### [versions](../src/versions)
-
-This directory contains everything that is dependent on the version of Coq that
-one wants to use. `standard` contains libraries for the standard version of Coq
-and `native` contains everything related to native Coq. Note that some
-libraries are already present in the default libraries of native Coq, in this
-case they have a counterpart in `standard` that replicates the functionality
-(without using native integers or native arrays).
-
-A particular point of interest is the files
-[smtcoq_plugin_standard.ml4](../src/versions/standard/smtcoq_plugin_standard.ml4)
-and
-[smtcoq_plugin_native.ml4](../src/versions/native/smtcoq_plugin_native.ml4). They
-provide extension points for Coq by defining new vernacular commands and new
-tactics. For instance the tactic `verit` tells Coq to call the OCaml function
-`verit.tactic` (which in turns uses the Coq API to manipulate the goals and
-call the certified checkers).
-
-```ocaml
-TACTIC EXTEND Tactic_verit
-| [ "verit" ] -> [ Verit.tactic () ]
-END
-```
-
 
 
 ### [spl](../src/spl)
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/Array/PArray.v
index 25da052..25da052 100644
--- a/src/versions/standard/Array/PArray_standard.v
+++ b/src/Array/PArray.v
diff --git a/src/versions/standard/Int63/Int63_standard.v b/src/Int63/Int63.v
index acee305..acee305 100644
--- a/src/versions/standard/Int63/Int63_standard.v
+++ b/src/Int63/Int63.v
diff --git a/src/versions/standard/Int63/Int63Axioms_standard.v b/src/Int63/Int63Axioms.v
index 9625bce..9625bce 100644
--- a/src/versions/standard/Int63/Int63Axioms_standard.v
+++ b/src/Int63/Int63Axioms.v
diff --git a/src/versions/standard/Int63/Int63Native_standard.v b/src/Int63/Int63Native.v
index 0f9d6b7..0f9d6b7 100644
--- a/src/versions/standard/Int63/Int63Native_standard.v
+++ b/src/Int63/Int63Native.v
diff --git a/src/versions/standard/Int63/Int63Op_standard.v b/src/Int63/Int63Op.v
index bb7d9a1..bb7d9a1 100644
--- a/src/versions/standard/Int63/Int63Op_standard.v
+++ b/src/Int63/Int63Op.v
diff --git a/src/versions/standard/Int63/Int63Properties_standard.v b/src/Int63/Int63Properties.v
index feb19b8..feb19b8 100644
--- a/src/versions/standard/Int63/Int63Properties_standard.v
+++ b/src/Int63/Int63Properties.v
diff --git a/src/versions/standard/Makefile.local b/src/Makefile.local
index 8abc72c..8abc72c 100644
--- a/src/versions/standard/Makefile.local
+++ b/src/Makefile.local
diff --git a/src/versions/standard/Tactics_standard.v b/src/Tactics.v
index f79b253..f79b253 100644
--- a/src/versions/standard/Tactics_standard.v
+++ b/src/Tactics.v
diff --git a/src/Trace.v b/src/Trace.v
index f9731f8..b6715ab 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -11,7 +11,6 @@
 
 
 Require Import Bool Int63 PArray.
-Require Structures.
 Require Import Misc State SMT_terms.
 Require Import Syntactic Arithmetic Operators Assumptions.
 Require Import Cnf Euf Lia BVList Bva_checker Array_checker.
@@ -34,7 +33,7 @@ Section trace.
 
   Variable rho : Valuation.t.
 
-  Definition _trace_ := Structures.trace step.
+  Definition _trace_ := ((list step) * step)%type.
 
   (* A checker for such a trace *)
 
@@ -42,7 +41,7 @@ Section trace.
   Hypothesis is_false_correct : forall c, is_false c -> ~ C.interp rho c.
 
   Definition _checker_ (s: S.t) (t: _trace_) (confl:clause_id) : bool :=
-    let s' := Structures.trace_fold check_step s t in
+    let s' := List.fold_left check_step (fst t) s in
     (* let s' := PArray.fold_left (fun s a => PArray.fold_left check_step s a) s t in *)
     is_false (S.get s' confl).
   (* Register _checker_ as PrimInline. *)
@@ -78,7 +77,11 @@ Section trace.
     intros s t' cid Hf Hv.
     apply (is_false_correct Hf).
     apply S.valid_get.
-    apply Structures.trace_fold_ind; auto.
+    clear Hf.
+    rewrite <- List.fold_left_rev_right in *.
+    induction (List.rev (fst t')); [ apply Hv | ].
+    apply valid_check_step.
+    apply IHl.
     (* apply PArray.fold_left_ind; auto. *)
     (* intros a i _ Ha;apply PArray.fold_left_ind;trivial. *)
     (* intros a0 i0 _ H1;auto. *)
@@ -534,7 +537,7 @@ Inductive step :=
   Definition setup_checker_step_debug d used_roots (c:certif) :=
     let (nclauses, t, confl) := c in
     let s := add_roots (S.make nclauses) d used_roots in
-    (s, Structures.trace_to_list t).
+    (s, fst t).
 
 
   Definition position_of_step (st:step) :=
@@ -686,7 +689,7 @@ Inductive step :=
     let (nclauses, t, confl) := c in
     let s := add_roots (S.make nclauses) d used_roots in
     let '(_, nb, failure) :=
-        Structures.trace_fold
+        List.fold_left
           (fun acc step =>
              match acc with
              | (s, nb, None) =>
@@ -698,7 +701,7 @@ Inductive step :=
                else (s, nb, None)
              | _ => acc
              end
-          ) (s, O, None) t
+          ) (fst t) (s, O, None)
     in
     match failure with
     | Some st => Some (nb, name_of_step st)
diff --git a/src/versions/standard/_CoqProject b/src/_CoqProject
index 133565d..f7862e1 100644
--- a/src/versions/standard/_CoqProject
+++ b/src/_CoqProject
@@ -26,21 +26,16 @@
 -I trace
 -I verit
 -I zchaff
--I versions/standard
--I versions/standard/Int63
--I versions/standard/Array
+-I Int63
+-I Array
 -I ../3rdparty/alt-ergo
 
-versions/standard/Int63/Int63.v
-versions/standard/Int63/Int63Native.v
-versions/standard/Int63/Int63Op.v
-versions/standard/Int63/Int63Axioms.v
-versions/standard/Int63/Int63Properties.v
-versions/standard/Array/PArray.v
-
-versions/standard/Structures.v
-versions/standard/structures.ml
-versions/standard/structures.mli
+Int63/Int63.v
+Int63/Int63Native.v
+Int63/Int63Op.v
+Int63/Int63Axioms.v
+Int63/Int63Properties.v
+Array/PArray.v
 
 bva/BVList.v
 bva/Bva_checker.v
@@ -73,6 +68,8 @@ trace/smtMisc.ml
 trace/smtMisc.mli
 trace/smtTrace.ml
 trace/smtTrace.mli
+trace/coqInterface.ml
+trace/coqInterface.mli
 
 ../3rdparty/alt-ergo/smtlib2_parse.ml
 ../3rdparty/alt-ergo/smtlib2_parse.mli
diff --git a/src/bva/Bva_checker.v b/src/bva/Bva_checker.v
index 7a47c70..1487453 100644
--- a/src/bva/Bva_checker.v
+++ b/src/bva/Bva_checker.v
@@ -12,8 +12,6 @@
 
 (** A small checker for bit-vectors bit-blasting *)
 
-Require Structures.
-
 Require Import Int63 Int63Properties PArray SMT_classes ZArith.
 
 Require Import Misc State SMT_terms BVList Psatz.
@@ -925,7 +923,7 @@ Definition shl_lit_be (a: list _lit) (b: list bool): list _lit :=
 
 
  Definition check_shl (bs1: list _lit) (bs2: list bool) (bsres: list _lit) : bool :=
-    if (Structures.nat_eqb (length bs1) (length bs2)) then
+    if (Nat.eqb (length bs1) (length bs2)) then
       if (forallb2 eq_carry_lit (lit_to_carry (shl_lit_be bs1 bs2)) bsres)
       then true else false
     else false.
@@ -976,7 +974,7 @@ Definition shr_lit_be (a: list _lit) (b: list bool): list _lit :=
 
 
  Definition check_shr (bs1: list _lit) (bs2: list bool) (bsres: list _lit) : bool :=
-    if (Structures.nat_eqb (length bs1) (length bs2)) then
+    if (Nat.eqb (length bs1) (length bs2)) then
       if (forallb2 eq_carry_lit (lit_to_carry (shr_lit_be bs1 bs2)) bsres)
       then true else false
     else false.
@@ -7946,7 +7944,7 @@ Proof. intro bs1.
        - simpl in *.
          unfold check_shl in H. simpl in H.
          case_eq bs2; simpl; intros; subst. simpl in H. now contradict H.
-         simpl in *. inversion H0. rewrite H2, Structures.nat_eqb_refl in H.
+         simpl in *. inversion H0. rewrite H2, Nat.eqb_refl in H.
          case_eq (forallb2 eq_carry_lit (lit_to_carry (shl_lit_be (a :: bs1) (b :: l))) bsres); intros.
          +  apply prop_eq_carry_lit2 in H1.
             rewrite prop_interp_carry3 in H1.
@@ -8016,8 +8014,8 @@ Proof. intro bs1.
        induction bs1 as [ | xbs1 xsbs1 IHbs1 ].
        - intros. simpl.
          unfold check_shl, shl_lit_be in H.
-         case_eq (Structures.nat_eqb (@length int []) (length bs2)); intros.
-         rewrite Structures.nat_eqb_eq in H0.
+         case_eq (Nat.eqb (@length int []) (length bs2)); intros.
+         rewrite Nat.eqb_eq in H0.
          rewrite <- H0 in H. simpl in H.
          rewrite nshl_lit_empty in H.
          case_eq bsres; intros. simpl.
@@ -8025,7 +8023,7 @@ Proof. intro bs1.
          subst; now contradict H.
          rewrite H0 in H; now contradict H.
        - intros. unfold check_shl in H.
-         case_eq (Structures.nat_eqb (Datatypes.length (xbs1 :: xsbs1)) (Datatypes.length bs2)); intros.
+         case_eq (Nat.eqb (Datatypes.length (xbs1 :: xsbs1)) (Datatypes.length bs2)); intros.
          rewrite H0 in H.
          case_eq (
           forallb2 eq_carry_lit (lit_to_carry (shl_lit_be (xbs1 :: xsbs1) bs2)) bsres); intros.
@@ -8033,7 +8031,7 @@ Proof. intro bs1.
          rewrite prop_interp_carry3 in H1.
          
          unfold RAWBITVECTOR_LIST.bv_shl.
-         rewrite Structures.nat_eqb_eq in H0.
+         rewrite Nat.eqb_eq in H0.
          unfold RAWBITVECTOR_LIST.size.
          rewrite !map_length. rewrite H0, N.eqb_refl.
          now rewrite <- H1, shl_interp.
@@ -8287,7 +8285,7 @@ Proof. intro bs1.
        - simpl in *.
          unfold check_shr in H. simpl in H.
          case_eq bs2; simpl; intros; subst. simpl in H. now contradict H.
-         simpl in *. inversion H0. rewrite H2, Structures.nat_eqb_refl in H.
+         simpl in *. inversion H0. rewrite H2, Nat.eqb_refl in H.
          case_eq (forallb2 eq_carry_lit (lit_to_carry (shr_lit_be (a :: bs1) (b :: l))) bsres); intros.
          +  apply prop_eq_carry_lit2 in H1.
             rewrite prop_interp_carry3 in H1.
@@ -8345,8 +8343,8 @@ Proof. intro bs1.
        induction bs1 as [ | xbs1 xsbs1 IHbs1 ].
        - intros. simpl.
          unfold check_shr, shr_lit_be in H.
-         case_eq (Structures.nat_eqb (@length int []) (length bs2)); intros.
-         rewrite Structures.nat_eqb_eq in H0.
+         case_eq (Nat.eqb (@length int []) (length bs2)); intros.
+         rewrite Nat.eqb_eq in H0.
          rewrite <- H0 in H. simpl in H.
          rewrite nshr_lit_empty in H.
          case_eq bsres; intros. simpl.
@@ -8354,7 +8352,7 @@ Proof. intro bs1.
          subst; now contradict H.
          rewrite H0 in H; now contradict H.
        - intros. unfold check_shr in H.
-         case_eq (Structures.nat_eqb (Datatypes.length (xbs1 :: xsbs1)) (Datatypes.length bs2)); intros.
+         case_eq (Nat.eqb (Datatypes.length (xbs1 :: xsbs1)) (Datatypes.length bs2)); intros.
          rewrite H0 in H.
          case_eq (
           forallb2 eq_carry_lit (lit_to_carry (shr_lit_be (xbs1 :: xsbs1) bs2)) bsres); intros.
@@ -8362,7 +8360,7 @@ Proof. intro bs1.
          rewrite prop_interp_carry3 in H1.
          
          unfold RAWBITVECTOR_LIST.bv_shr.
-         rewrite Structures.nat_eqb_eq in H0.
+         rewrite Nat.eqb_eq in H0.
          unfold RAWBITVECTOR_LIST.size.
          rewrite !map_length. rewrite H0, N.eqb_refl.
          now rewrite <- H1, shr_interp.
diff --git a/src/classes/SMT_classes_instances.v b/src/classes/SMT_classes_instances.v
index aa2082e..a2831cf 100644
--- a/src/classes/SMT_classes_instances.v
+++ b/src/classes/SMT_classes_instances.v
@@ -13,7 +13,6 @@
 Require Import Bool OrderedType BinPos ZArith OrderedTypeEx.
 Require Import Int63.
 Require Import State BVList FArray.
-Require Structures.
 Require Export SMT_classes.
 
 
@@ -253,7 +252,7 @@ Section Nat.
   Defined.
 
   Global Instance Nat_eqbtype : EqbType nat :=
-    {| eqb := Structures.nat_eqb; eqb_spec := Structures.nat_eqb_eq |}.
+    {| eqb := Nat.eqb; eqb_spec := Nat.eqb_eq |}.
 
   Global Instance Nat_dec : DecType nat := EqbToDecType.
 
diff --git a/src/configure.sh b/src/configure.sh
deleted file mode 100755
index fb265e0..0000000
--- a/src/configure.sh
+++ /dev/null
@@ -1,42 +0,0 @@
-#!/bin/sh
-
-pre=$(echo $0 | sed "s,\(\([^/]*/\)*\)[^/]*,\1,")
-
-rm -f ${pre}_CoqProject
-rm -f ${pre}Makefile
-rm -f ${pre}Makefile.conf
-rm -f ${pre}Makefile.local
-rm -f ${pre}smtcoq_plugin.ml4
-rm -f ${pre}versions/native/Structures.v
-rm -f ${pre}g_smtcoq.mlg
-rm -f ${pre}smtcoq_plugin.mlpack
-rm -f ${pre}Tactics.v
-rm -f ${pre}versions/standard/Int63/Int63.v
-rm -f ${pre}versions/standard/Int63/Int63Native.v
-rm -f ${pre}versions/standard/Int63/Int63Op.v
-rm -f ${pre}versions/standard/Int63/Int63Axioms.v
-rm -f ${pre}versions/standard/Int63/Int63Properties.v
-rm -f ${pre}versions/standard/Array/PArray.v
-rm -f ${pre}versions/standard/Structures.v
-
-set -e
-if [ $@ -a $@ = -native ]; then
-    cp ${pre}versions/native/Makefile ${pre}Makefile
-    cp ${pre}versions/native/smtcoq_plugin_native.ml4 ${pre}smtcoq_plugin.ml4
-    cp ${pre}versions/native/Structures_native.v ${pre}versions/native/Structures.v
-    cp ${pre}versions/native/Tactics_native.v ${pre}Tactics.v
-else
-    cp ${pre}versions/standard/_CoqProject ${pre}_CoqProject
-    cp ${pre}versions/standard/Makefile.local ${pre}Makefile.local
-    cp ${pre}versions/standard/g_smtcoq_standard.mlg ${pre}g_smtcoq.mlg
-    cp ${pre}versions/standard/smtcoq_plugin_standard.mlpack ${pre}smtcoq_plugin.mlpack
-    cp ${pre}versions/standard/Int63/Int63_standard.v ${pre}versions/standard/Int63/Int63.v
-    cp ${pre}versions/standard/Int63/Int63Native_standard.v ${pre}versions/standard/Int63/Int63Native.v
-    cp ${pre}versions/standard/Int63/Int63Op_standard.v ${pre}versions/standard/Int63/Int63Op.v
-    cp ${pre}versions/standard/Int63/Int63Axioms_standard.v ${pre}versions/standard/Int63/Int63Axioms.v
-    cp ${pre}versions/standard/Int63/Int63Properties_standard.v ${pre}versions/standard/Int63/Int63Properties.v
-    cp ${pre}versions/standard/Array/PArray_standard.v ${pre}versions/standard/Array/PArray.v
-    cp ${pre}versions/standard/Structures_standard.v ${pre}versions/standard/Structures.v
-    cp ${pre}versions/standard/Tactics_standard.v ${pre}Tactics.v
-    coq_makefile -f _CoqProject -o Makefile
-fi
diff --git a/src/extraction/Makefile b/src/extraction/Makefile
index 73b0ae4..354dd53 100644
--- a/src/extraction/Makefile
+++ b/src/extraction/Makefile
@@ -15,7 +15,7 @@ COQTOP=$(COQBIN)../
 FLAGS=-rectypes
 COMPILEFLAGS=-cclib -lunix
 
-SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../euf -I ../cnf -I ../versions/native/
+SMTLIB=-I .. -I ../zchaff -I ../verit -I ../trace -I ../smtlib2 -I ../lia -I ../euf -I ../cnf -I ../../3rdparty/alt-ergo
 COQLIB=-I ${COQTOP}kernel -I ${COQTOP}lib -I ${COQTOP}library -I ${COQTOP}parsing -I ${COQTOP}pretyping -I ${COQTOP}interp -I ${COQTOP}proofs -I ${COQTOP}tactics -I ${COQTOP}toplevel -I ${COQTOP}plugins/btauto -I ${COQTOP}plugins/cc -I ${COQTOP}plugins/decl_mode -I ${COQTOP}plugins/extraction -I ${COQTOP}plugins/field -I ${COQTOP}plugins/firstorder -I ${COQTOP}plugins/fourier -I ${COQTOP}plugins/funind -I ${COQTOP}plugins/micromega -I ${COQTOP}plugins/nsatz -I ${COQTOP}plugins/omega -I ${COQTOP}plugins/quote -I ${COQTOP}plugins/ring -I ${COQTOP}plugins/romega -I ${COQTOP}plugins/rtauto -I ${COQTOP}plugins/setoid_ring -I ${COQTOP}plugins/syntax -I ${COQTOP}plugins/xml -I /usr/lib/ocaml/camlp5
 
 CMXA=nums.cmxa str.cmxa unix.cmxa gramlib.cmxa dynlink.cmxa ${COQTOP}kernel/byterun/coq_fix_code.o ${COQTOP}kernel/byterun/coq_interp.o ${COQTOP}kernel/byterun/coq_memory.o ${COQTOP}kernel/byterun/coq_values.o clib.cmxa lib.cmxa kernel.cmxa library.cmxa pretyping.cmxa interp.cmxa proofs.cmxa parsing.cmxa tactics.cmxa toplevel.cmxa micromega_plugin.cmxa smtcoq.cmxa
diff --git a/src/extraction/verit_checker.mli b/src/extraction/verit_checker.mli
index 4491410..7b8b882 100644
--- a/src/extraction/verit_checker.mli
+++ b/src/extraction/verit_checker.mli
@@ -10,7 +10,7 @@
 (**************************************************************************)
 
 
-module Mc = Structures.Micromega_plugin_Certificate.Mc
+module Mc = CoqInterface.Micromega_plugin_Certificate.Mc
 val mkInt : int -> ExtrNative.uint
 val mkArray : 'a array -> 'a ExtrNative.parray
 val dump_nat : Mc.nat -> Smt_checker.nat
@@ -25,7 +25,7 @@ val to_coq :
   'a SmtCertif.clause ->
   Smt_checker.Euf_Checker.step ExtrNative.parray ExtrNative.parray *
   'a SmtCertif.clause
-val btype_to_coq : SmtAtom.btype -> Smt_checker.Typ.coq_type
+val btype_to_coq : SmtBtype.btype -> Smt_checker.Typ.coq_type
 val c_to_coq : SmtAtom.cop -> Smt_checker.Atom.cop
 val u_to_coq : SmtAtom.uop -> Smt_checker.Atom.unop
 val b_to_coq : SmtAtom.bop -> Smt_checker.Atom.binop
@@ -42,7 +42,7 @@ val form_interp_tbl :
   SmtAtom.Form.reify -> Smt_checker.Form.form ExtrNative.parray
 val count_btype : int ref
 val count_op : int ref
-val declare_sort : Smtlib2_ast.symbol -> SmtAtom.btype
+val declare_sort : Smtlib2_ast.symbol -> SmtBtype.btype
 val declare_fun :
   Smtlib2_ast.symbol ->
   Smtlib2_ast.sort list -> Smtlib2_ast.sort -> SmtAtom.indexed_op
diff --git a/src/versions/standard/g_smtcoq_standard.mlg b/src/g_smtcoq.mlg
index 5cfb287..c8d38db 100644
--- a/src/versions/standard/g_smtcoq_standard.mlg
+++ b/src/g_smtcoq.mlg
@@ -87,7 +87,7 @@ let lemmas_list = Summary.ref ~name:"Selected lemmas" []
 let cache_lemmas (_, lems) =
   lemmas_list := lems
 
-let declare_lemmas : Structures.constr_expr list -> Libobject.obj =
+let declare_lemmas : CoqInterface.constr_expr list -> Libobject.obj =
   let open Libobject in
   declare_object
     {
diff --git a/src/lfsc/lfsc.ml b/src/lfsc/lfsc.ml
index f17eb04..f2157a4 100644
--- a/src/lfsc/lfsc.ml
+++ b/src/lfsc/lfsc.ml
@@ -57,7 +57,7 @@ let process_signatures_once =
           ) signatures
       with
       | Ast.TypingError (t1, t2) ->
-        Structures.error
+        CoqInterface.error
           (asprintf "@[<hov>LFSC typing error: expected %a, got %a@]@."
              Ast.print_term t1
              Ast.print_term t2)
@@ -116,7 +116,7 @@ let import_trace first parse lexbuf =
 
   with
   | Ast.TypingError (t1, t2) ->
-    Structures.error
+    CoqInterface.error
       (asprintf "@[<hov>LFSC typing error: expected %a, got %a@]@."
          Ast.print_term t1
          Ast.print_term t2)
@@ -386,13 +386,13 @@ let call_cvc4 env rt ro ra rf root _ =
       begin
         try get_proof cvc4 (import_trace (Some root) lfsc_parse_one)
         with
-        | Ast.CVC4Sat -> Structures.error "CVC4 returned SAT"
-        | No_proof -> Structures.error "CVC4 did not generate a proof"
-        | Failure s -> Structures.error ("Importing of proof failed: " ^ s)
+        | Ast.CVC4Sat -> CoqInterface.error "CVC4 returned SAT"
+        | No_proof -> CoqInterface.error "CVC4 did not generate a proof"
+        | Failure s -> CoqInterface.error ("Importing of proof failed: " ^ s)
       end
     | Sat ->
       let smodel = get_model cvc4 in
-      Structures.error
+      CoqInterface.error
         ("CVC4 returned sat. Here is the model:\n\n" ^
          SmtCommands.model_string env rt ro ra rf smodel)
         (* (asprintf "CVC4 returned sat. Here is the model:\n%a" SExpr.print smodel) *)
@@ -435,7 +435,7 @@ let get_model_from_file filename =
   let lexbuf = Lexing.from_channel chan in
   match SExprParser.sexps SExprLexer.main lexbuf with
   | [SExpr.Atom "sat"; m] -> m
-  | _ -> Structures.error "CVC4 returned SAT but no model"
+  | _ -> CoqInterface.error "CVC4 returned SAT but no model"
 
 
 let call_cvc4_file env rt ro ra rf root =
@@ -467,17 +467,17 @@ let call_cvc4_file env rt ro ra rf root =
   eprintf "CVC4 = %.5f@." (t1-.t0);
 
   if exit_code <> 0 then
-    Structures.error ("CVC4 crashed: return code "^string_of_int exit_code);
+    CoqInterface.error ("CVC4 crashed: return code "^string_of_int exit_code);
 
   (* ignore (Sys.command clean_cmd); *)
 
   try import_trace_from_file (Some root) prooffilename
   with
-  | No_proof -> Structures.error "CVC4 did not generate a proof"
-  | Failure s -> Structures.error ("Importing of proof failed: " ^ s)
+  | No_proof -> CoqInterface.error "CVC4 did not generate a proof"
+  | Failure s -> CoqInterface.error ("Importing of proof failed: " ^ s)
   | Ast.CVC4Sat ->
     let smodel = get_model_from_file prooffilename in
-    Structures.error
+    CoqInterface.error
       ("CVC4 returned sat. Here is the model:\n\n" ^
        SmtCommands.model_string env rt ro ra rf smodel)
 
diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index 53dbf6d..e00092e 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -12,7 +12,7 @@
 
 (*** Linking SMT Terms to Micromega Terms ***)
 open Util
-open Structures.Micromega_plugin_Micromega
+open CoqInterface.Micromega_plugin_Micromega
 
 open SmtForm
 open SmtAtom
@@ -92,7 +92,7 @@ let smt_binop_to_micromega_formula tbl op ha hb =
     | BO_Zge -> OpGe
     | BO_Zgt -> OpGt
     | BO_eq _ -> OpEq
-    | _ -> Structures.error
+    | _ -> CoqInterface.error
 	  "lia.ml: smt_binop_to_micromega_formula expecting a formula"
   in
   let lhs = smt_Atom_to_micromega_pExpr tbl ha in
@@ -102,7 +102,7 @@ let smt_binop_to_micromega_formula tbl op ha hb =
 let smt_Atom_to_micromega_formula tbl ha =
   match Atom.atom ha with
     | Abop (op,ha,hb) -> smt_binop_to_micromega_formula tbl op ha hb
-    | _ -> Structures.error
+    | _ -> CoqInterface.error
 	  "lia.ml: smt_Atom_to_micromega_formula was expecting an LIA formula"
 
 (* specialized fold *)
@@ -152,7 +152,7 @@ let smt_clause_to_coq_micromega_formula tbl cl =
   binop_list tbl (fun x y -> Cj (x,y)) TT (List.map Form.neg cl)
 
 let tauto_lia ff =
-  let cnf_ff,_ = Structures.Micromega_plugin_Micromega.cnfZ ff in
+  let cnf_ff,_ = CoqInterface.Micromega_plugin_Micromega.cnfZ ff in
  let rec xwitness_list l =
   match l with
    | [] -> Some []
@@ -160,8 +160,8 @@ let tauto_lia ff =
       match xwitness_list l with
       | None -> None
       | Some l ->
-         match Structures.Micromega_plugin_Certificate.lia true max_int (List.map (fun ((e, o), _) -> Structures.Micromega_plugin_Micromega.denorm e, o) e) with
-         | Structures.Micromega_plugin_Certificate.Prf w -> Some (w::l)
+         match CoqInterface.Micromega_plugin_Certificate.lia true max_int (List.map (fun ((e, o), _) -> CoqInterface.Micromega_plugin_Micromega.denorm e, o) e) with
+         | CoqInterface.Micromega_plugin_Certificate.Prf w -> Some (w::l)
          | _ -> None in
  xwitness_list cnf_ff
 
diff --git a/src/lia/lia.mli b/src/lia/lia.mli
index 7b4c6c8..f996ac0 100644
--- a/src/lia/lia.mli
+++ b/src/lia/lia.mli
@@ -12,4 +12,4 @@
 
 val build_lia_certif :
   SmtAtom.Form.t list ->
-  Structures.Micromega_plugin_Certificate.Mc.zArithProof list option
+  CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list option
diff --git a/src/versions/standard/smtcoq_plugin_standard.mlpack b/src/smtcoq_plugin.mlpack
index f210db1..0907551 100644
--- a/src/versions/standard/smtcoq_plugin_standard.mlpack
+++ b/src/smtcoq_plugin.mlpack
@@ -1,4 +1,4 @@
-Structures
+CoqInterface
 
 SmtMisc
 CoqTerms
diff --git a/src/smtlib2/smtlib2_genConstr.ml b/src/smtlib2/smtlib2_genConstr.ml
index eb1c5b7..0c6e2ac 100644
--- a/src/smtlib2/smtlib2_genConstr.ml
+++ b/src/smtlib2/smtlib2_genConstr.ml
@@ -97,10 +97,10 @@ let rec sort_of_sort = function
 
 
 let declare_sort_from_name rt s =
-  let cons_t = Structures.declare_new_type (Structures.mkId ("Smt_sort_"^s)) in
+  let cons_t = CoqInterface.declare_new_type (CoqInterface.mkId ("Smt_sort_"^s)) in
   let compdec_type = mklApp cCompDec [| cons_t |] in
   let compdec_var =
-    Structures.declare_new_variable (Structures.mkId ("CompDec_"^s)) compdec_type in
+    CoqInterface.declare_new_variable (CoqInterface.mkId ("CompDec_"^s)) compdec_type in
   let res = SmtBtype.of_coq_compdec rt cons_t compdec_var in
   SmtMaps.add_btype s res;
   res
@@ -110,9 +110,9 @@ let declare_sort rt sym = declare_sort_from_name rt (string_of_symbol sym)
 
 let declare_fun_from_name rt ro s tyl ty =
   let coqTy = List.fold_right (fun typ c ->
-      Structures.mkArrow (interp_to_coq rt typ) c)
+      CoqInterface.mkArrow (interp_to_coq rt typ) c)
       tyl (interp_to_coq rt ty) in
-  let cons_v = Structures.declare_new_variable (Structures.mkId ("Smt_var_"^s)) coqTy in
+  let cons_v = CoqInterface.declare_new_variable (CoqInterface.mkId ("Smt_var_"^s)) coqTy in
   let op = Op.declare ro cons_v (Array.of_list tyl) ty None in
   SmtMaps.add_fun s op;
   op
diff --git a/src/smtlib2/smtlib2_solver.ml b/src/smtlib2/smtlib2_solver.ml
index 99538ce..efab1c1 100644
--- a/src/smtlib2/smtlib2_solver.ml
+++ b/src/smtlib2/smtlib2_solver.ml
@@ -73,7 +73,7 @@ let read_response { lexbuf } =
 
 let error s sexp =
   kill s;
-  Structures.error (asprintf "Solver error: %a." SExpr.print sexp)
+  CoqInterface.error (asprintf "Solver error: %a." SExpr.print sexp)
 
 
 let read_success s = 
@@ -89,7 +89,7 @@ let read_check_result s =
   match SExprParser.sexp SExprLexer.main s.lexbuf with
   | SExpr.Atom "sat" -> Sat
   | SExpr.Atom "unsat" -> Unsat
-  | SExpr.Atom "unknown" -> Structures.error ("Solver returned uknown.")
+  | SExpr.Atom "unknown" -> CoqInterface.error ("Solver returned uknown.")
   | r -> error s r
 
 
@@ -111,7 +111,7 @@ let send_command s cmd read =
      *   let buf = Bytes.create err_p2 in
      *   Unix.read s.stderr buf 0 err_p2 |> ignore;
      *   let err_msg = Bytes.sub_string buf err_p1 len in
-     *   Structures.error ("Solver error: "^err_msg);
+     *   CoqInterface.error ("Solver error: "^err_msg);
      * end
      * else (kill s; raise e) *)
     kill s; raise e
diff --git a/src/versions/standard/structures.ml b/src/trace/coqInterface.ml
index 863c921..36f4337 100644
--- a/src/versions/standard/structures.ml
+++ b/src/trace/coqInterface.ml
@@ -112,7 +112,7 @@ let init_modules = Coqlib.init_modules
 
 
 (* Int63 *)
-let int63_modules = [["SMTCoq";"versions";"standard";"Int63";"Int63Native"]]
+let int63_modules = [["SMTCoq";"Int63";"Int63Native"]]
 
 (* 31-bits integers are "called" 63 bits (this is sound) *)
 let int31_module = [["Coq";"Numbers";"Cyclic";"Int31";"Int31"]]
@@ -135,7 +135,7 @@ let cint = gen_constant int31_module "int31"
 
 
 (* PArray *)
-let parray_modules = [["SMTCoq";"versions";"standard";"Array";"PArray"]]
+let parray_modules = [["SMTCoq";"Array";"PArray"]]
 
 let cmake = gen_constant parray_modules "make"
 let cset = gen_constant parray_modules "set"
diff --git a/src/versions/standard/structures.mli b/src/trace/coqInterface.mli
index 104f3f9..104f3f9 100644
--- a/src/versions/standard/structures.mli
+++ b/src/trace/coqInterface.mli
diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index c6188b8..1c4ee81 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -13,23 +13,23 @@
 open SmtMisc
 
 
-let gen_constant = Structures.gen_constant
+let gen_constant = CoqInterface.gen_constant
 
 
 (* Int63 *)
-let cint = Structures.cint
-let ceq63 = gen_constant Structures.int63_modules "eqb"
+let cint = CoqInterface.cint
+let ceq63 = gen_constant CoqInterface.int63_modules "eqb"
 
 (* PArray *)
-let carray = gen_constant Structures.parray_modules "array"
+let carray = gen_constant CoqInterface.parray_modules "array"
 
 (* is_true *)
-let cis_true = gen_constant Structures.init_modules "is_true"
+let cis_true = gen_constant CoqInterface.init_modules "is_true"
 
 (* nat *)
-let cnat = gen_constant Structures.init_modules "nat"
-let cO = gen_constant Structures.init_modules "O"
-let cS = gen_constant Structures.init_modules "S"
+let cnat = gen_constant CoqInterface.init_modules "nat"
+let cO = gen_constant CoqInterface.init_modules "O"
+let cS = gen_constant CoqInterface.init_modules "S"
 
 (* Positive *)
 let positive_modules = [["Coq";"Numbers";"BinNums"];
@@ -74,49 +74,49 @@ let ceqbZ = gen_constant z_modules "eqb"
 (* Booleans *)
 let bool_modules = [["Coq";"Bool";"Bool"]]
 
-let cbool = gen_constant Structures.init_modules "bool"
-let ctrue = gen_constant Structures.init_modules "true"
-let cfalse = gen_constant Structures.init_modules "false"
-let candb = gen_constant Structures.init_modules "andb"
-let corb = gen_constant Structures.init_modules "orb"
-let cxorb = gen_constant Structures.init_modules "xorb"
-let cnegb = gen_constant Structures.init_modules "negb"
-let cimplb = gen_constant Structures.init_modules "implb"
+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 Structures.init_modules "iff"
+let ciff = gen_constant CoqInterface.init_modules "iff"
 let creflect = gen_constant bool_modules "reflect"
 
 (* Lists *)
-let clist = gen_constant Structures.init_modules "list"
-let cnil = gen_constant Structures.init_modules "nil"
-let ccons = gen_constant Structures.init_modules "cons"
-let clength = gen_constant Structures.init_modules "length"
+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"
 
 (* Option *)
-let coption = gen_constant Structures.init_modules "option"
-let cSome = gen_constant Structures.init_modules "Some"
-let cNone = gen_constant Structures.init_modules "None"
+let coption = gen_constant CoqInterface.init_modules "option"
+let cSome = gen_constant CoqInterface.init_modules "Some"
+let cNone = gen_constant CoqInterface.init_modules "None"
 
 (* Pairs *)
-let cpair = gen_constant Structures.init_modules "pair"
-let cprod = gen_constant Structures.init_modules "prod"
+let cpair = gen_constant CoqInterface.init_modules "pair"
+let cprod = gen_constant CoqInterface.init_modules "prod"
 
 (* Dependent pairs *)
-let csigT = gen_constant Structures.init_modules "sigT"
-(* let cprojT1 = gen_constant Structures.init_modules "projT1" *)
-(* let cprojT2 = gen_constant Structures.init_modules "projT2" *)
-(* let cprojT3 = gen_constant Structures.init_modules "projT3" *)
+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 Structures.init_modules "sigT2" *)
-(* let csigT_of_sigT2 = gen_constant Structures.init_modules "sigT_of_sigT2" *)
+(* let csigT2 = gen_constant CoqInterface.init_modules "sigT2" *)
+(* let csigT_of_sigT2 = gen_constant CoqInterface.init_modules "sigT_of_sigT2" *)
 
 (* Logical Operators *)
-let cnot = gen_constant Structures.init_modules "not"
-let ceq = gen_constant Structures.init_modules "eq"
-let crefl_equal = gen_constant Structures.init_modules "eq_refl"
-let cconj = gen_constant Structures.init_modules "conj"
-let cand = gen_constant Structures.init_modules "and"
+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"
 
 (* Bit vectors *)
 let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]]
@@ -306,8 +306,8 @@ let ceq_refl_true =
 let eq_refl_true () = Lazy.force ceq_refl_true
 
 let vm_cast_true_no_check t =
-  Structures.mkCast(eq_refl_true (),
-              Structures.vmcast,
+  CoqInterface.mkCast(eq_refl_true (),
+              CoqInterface.vmcast,
               mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|])
 
 (* This version checks convertibility right away instead of delaying it at
@@ -315,13 +315,13 @@ let vm_cast_true_no_check t =
    SMTCoq's tactics. *)
 let vm_cast_true env t =
   try
-    Structures.vm_conv Reduction.CUMUL env
+    CoqInterface.vm_conv Reduction.CUMUL env
       (mklApp ceq
          [|Lazy.force cbool; Lazy.force ctrue; Lazy.force ctrue|])
       (mklApp ceq [|Lazy.force cbool; t; Lazy.force ctrue|]);
     vm_cast_true_no_check t
   with Reduction.NotConvertible ->
-    Structures.error ("SMTCoq was not able to check the proof certificate.")
+    CoqInterface.error ("SMTCoq was not able to check the proof certificate.")
 
 
 (* Compute a nat *)
@@ -355,39 +355,39 @@ let rec mk_bv_list = function
 
 (* Reification *)
 let mk_bool b =
-  let c, args = Structures.decompose_app b in
-  if Structures.eq_constr c (Lazy.force ctrue) then true
-  else if Structures.eq_constr c (Lazy.force cfalse) then false
+  let c, args = CoqInterface.decompose_app b in
+  if CoqInterface.eq_constr c (Lazy.force ctrue) then true
+  else if CoqInterface.eq_constr c (Lazy.force cfalse) then false
   else assert false
 
 let rec mk_bool_list bs =
-  let c, args = Structures.decompose_app bs in
-  if Structures.eq_constr c (Lazy.force cnil) then []
-  else if Structures.eq_constr c (Lazy.force ccons) then
+  let c, args = CoqInterface.decompose_app bs in
+  if CoqInterface.eq_constr c (Lazy.force cnil) then []
+  else if CoqInterface.eq_constr c (Lazy.force ccons) then
     match args with
     | [_; b; bs] -> mk_bool b :: mk_bool_list bs
     | _ -> assert false
   else assert false
 
 let rec mk_nat n =
-  let c, args = Structures.decompose_app n in
-  if Structures.eq_constr c (Lazy.force cO) then
+  let c, args = CoqInterface.decompose_app n in
+  if CoqInterface.eq_constr c (Lazy.force cO) then
     0
-  else if Structures.eq_constr c (Lazy.force cS) then
+  else if CoqInterface.eq_constr c (Lazy.force cS) then
     match args with
     | [n] -> (mk_nat n) + 1
     | _ -> assert false
   else assert false
 
 let rec mk_positive n =
-  let c, args = Structures.decompose_app n in
-  if Structures.eq_constr c (Lazy.force cxH) then
+  let c, args = CoqInterface.decompose_app n in
+  if CoqInterface.eq_constr c (Lazy.force cxH) then
     1
-  else if Structures.eq_constr c (Lazy.force cxO) then
+  else if CoqInterface.eq_constr c (Lazy.force cxO) then
     match args with
     | [n] -> 2 * (mk_positive n)
     | _ -> assert false
-  else if Structures.eq_constr c (Lazy.force cxI) then
+  else if CoqInterface.eq_constr c (Lazy.force cxI) then
     match args with
     | [n] -> 2 * (mk_positive n) + 1
     | _ -> assert false
@@ -395,10 +395,10 @@ let rec mk_positive n =
 
 
 let mk_N n =
-  let c, args = Structures.decompose_app n in
-  if Structures.eq_constr c (Lazy.force cN0) then
+  let c, args = CoqInterface.decompose_app n in
+  if CoqInterface.eq_constr c (Lazy.force cN0) then
     0
-  else if Structures.eq_constr c (Lazy.force cNpos) then
+  else if CoqInterface.eq_constr c (Lazy.force cNpos) then
     match args with
     | [n] -> mk_positive n
     | _ -> assert false
@@ -406,13 +406,13 @@ let mk_N n =
 
 
 let mk_Z n =
-  let c, args = Structures.decompose_app n in
-  if Structures.eq_constr c (Lazy.force cZ0) then 0
-  else if Structures.eq_constr c (Lazy.force cZpos) then
+  let c, args = CoqInterface.decompose_app n in
+  if CoqInterface.eq_constr c (Lazy.force cZ0) then 0
+  else if CoqInterface.eq_constr c (Lazy.force cZpos) then
     match args with
     | [n] -> mk_positive n
     | _ -> assert false
-  else if Structures.eq_constr c (Lazy.force cZneg) then
+  else if CoqInterface.eq_constr c (Lazy.force cZneg) then
     match args with
     | [n] -> - mk_positive n
     | _ -> assert false
@@ -421,12 +421,12 @@ let mk_Z n =
 
 (* size of bivectors are either N.of_nat (length l) or an N *)
 let mk_bvsize n =
-  let c, args = Structures.decompose_app n in
-  if Structures.eq_constr c (Lazy.force cof_nat) then
+  let c, args = CoqInterface.decompose_app n in
+  if CoqInterface.eq_constr c (Lazy.force cof_nat) then
     match args with
     | [nl] ->
-      let c, args = Structures.decompose_app nl in
-      if Structures.eq_constr c (Lazy.force clength) then
+      let c, args = CoqInterface.decompose_app nl in
+      if CoqInterface.eq_constr c (Lazy.force clength) then
         match args with
         | [_; l] -> List.length (mk_bool_list l)
         | _ -> assert false
@@ -437,7 +437,7 @@ let mk_bvsize n =
 (** Switches between constr and OCaml *)
 (* Transform a option constr into a constr option *)
 let option_of_constr_option co =
-  let c, args = Structures.decompose_app co in
+  let c, args = CoqInterface.decompose_app co in
   if c = Lazy.force cSome then
     match args with
       | [_;c] -> Some c
@@ -448,7 +448,7 @@ let option_of_constr_option co =
 (* Transform a tuple of constr into a (reversed) list of constr *)
 let list_of_constr_tuple =
   let rec list_of_constr_tuple acc t =
-    let c, args = Structures.decompose_app t in
+    let c, args = CoqInterface.decompose_app t in
     if c = Lazy.force cpair then
       match args with
         | [_;_;t1;t2] ->
diff --git a/src/trace/coqTerms.mli b/src/trace/coqTerms.mli
index 282f8f6..92acbb6 100644
--- a/src/trace/coqTerms.mli
+++ b/src/trace/coqTerms.mli
@@ -10,258 +10,258 @@
 (**************************************************************************)
 
 
-val gen_constant : string list list -> string -> Structures.constr lazy_t
+val gen_constant : string list list -> string -> CoqInterface.constr lazy_t
 
 (* Int63 *)
-val cint : Structures.constr lazy_t
-val ceq63 : Structures.constr lazy_t
+val cint : CoqInterface.constr lazy_t
+val ceq63 : CoqInterface.constr lazy_t
 
 (* PArray *)
-val carray : Structures.constr lazy_t
+val carray : CoqInterface.constr lazy_t
 
 (* nat *)
-val cnat : Structures.constr lazy_t
-val cO : Structures.constr lazy_t
-val cS : Structures.constr lazy_t
+val cnat : CoqInterface.constr lazy_t
+val cO : CoqInterface.constr lazy_t
+val cS : CoqInterface.constr lazy_t
 
 (* Positive *)
-val cpositive : Structures.constr lazy_t
-val cxI : Structures.constr lazy_t
-val cxO : Structures.constr lazy_t
-val cxH : Structures.constr lazy_t
-val ceqbP : Structures.constr lazy_t
+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
 
 (* N *)
-val cN : Structures.constr lazy_t
-val cN0 : Structures.constr lazy_t
-val cNpos : Structures.constr lazy_t
-val cof_nat : Structures.constr lazy_t
+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
 
 (* Z *)
-val cZ : Structures.constr lazy_t
-val cZ0 : Structures.constr lazy_t
-val cZpos : Structures.constr lazy_t
-val cZneg : Structures.constr lazy_t
-val copp : Structures.constr lazy_t
-val cadd : Structures.constr lazy_t
-val csub : Structures.constr lazy_t
-val cmul : Structures.constr lazy_t
-val cltb : Structures.constr lazy_t
-val cleb : Structures.constr lazy_t
-val cgeb : Structures.constr lazy_t
-val cgtb : Structures.constr lazy_t
-val ceqbZ : Structures.constr lazy_t
+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
 
 (* Booleans *)
-val cbool : Structures.constr lazy_t
-val ctrue : Structures.constr lazy_t
-val cfalse : Structures.constr lazy_t
-val candb : Structures.constr lazy_t
-val corb : Structures.constr lazy_t
-val cxorb : Structures.constr lazy_t
-val cnegb : Structures.constr lazy_t
-val cimplb : Structures.constr lazy_t
-val ceqb : Structures.constr lazy_t
-val cifb : Structures.constr lazy_t
-val ciff : Structures.constr lazy_t
-val creflect : Structures.constr lazy_t
+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
 
 (* Lists *)
-val clist : Structures.constr lazy_t
-val cnil : Structures.constr lazy_t
-val ccons : Structures.constr lazy_t
-val clength : Structures.constr lazy_t
+val clist : CoqInterface.constr lazy_t
+val cnil : CoqInterface.constr lazy_t
+val ccons : CoqInterface.constr lazy_t
+val clength : CoqInterface.constr lazy_t
 
 (* Option *)
-val coption : Structures.constr lazy_t
-val cSome : Structures.constr lazy_t
-val cNone : Structures.constr lazy_t
+val coption : CoqInterface.constr lazy_t
+val cSome : CoqInterface.constr lazy_t
+val cNone : CoqInterface.constr lazy_t
 
 (* Pairs *)
-val cpair : Structures.constr lazy_t
-val cprod : Structures.constr lazy_t
+val cpair : CoqInterface.constr lazy_t
+val cprod : CoqInterface.constr lazy_t
 
 (* Dependent pairs *)
-val csigT : Structures.constr lazy_t
+val csigT : CoqInterface.constr lazy_t
 
 (* Logical Operators *)
-val cnot : Structures.constr lazy_t
-val ceq : Structures.constr lazy_t
-val crefl_equal : Structures.constr lazy_t
-val cconj : Structures.constr lazy_t
-val cand : Structures.constr lazy_t
+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
 
 (* Bit vectors *)
-val cbitvector : Structures.constr lazy_t
-val cof_bits : Structures.constr lazy_t
-val cbitOf : Structures.constr lazy_t
-val cbv_eq : Structures.constr lazy_t
-val cbv_not : Structures.constr lazy_t
-val cbv_neg : Structures.constr lazy_t
-val cbv_and : Structures.constr lazy_t
-val cbv_or : Structures.constr lazy_t
-val cbv_xor : Structures.constr lazy_t
-val cbv_add : Structures.constr lazy_t
-val cbv_mult : Structures.constr lazy_t
-val cbv_ult : Structures.constr lazy_t
-val cbv_slt : Structures.constr lazy_t
-val cbv_concat : Structures.constr lazy_t
-val cbv_extr : Structures.constr lazy_t
-val cbv_zextn : Structures.constr lazy_t
-val cbv_sextn : Structures.constr lazy_t
-val cbv_shl : Structures.constr lazy_t
-val cbv_shr : Structures.constr lazy_t
+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
 
 (* Arrays *)
-val cfarray : Structures.constr lazy_t
-val cselect : Structures.constr lazy_t
-val cstore : Structures.constr lazy_t
-val cdiff : Structures.constr lazy_t
-val cequalarray : Structures.constr lazy_t
+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 : Structures.constr lazy_t
-val cState_S_t : Structures.constr lazy_t
-
-val cdistinct : Structures.constr lazy_t
-
-val ctype : Structures.constr lazy_t
-val cTZ : Structures.constr lazy_t
-val cTbool : Structures.constr lazy_t
-val cTpositive : Structures.constr lazy_t
-val cTBV : Structures.constr lazy_t
-val cTFArray : Structures.constr lazy_t
-val cTindex : Structures.constr lazy_t
-
-val cinterp_t : Structures.constr lazy_t
-val cdec_interp : Structures.constr lazy_t
-val cord_interp : Structures.constr lazy_t
-val ccomp_interp : Structures.constr lazy_t
-val cinh_interp : Structures.constr lazy_t
-
-val cinterp_eqb : Structures.constr lazy_t
-
-val ctyp_compdec : Structures.constr lazy_t
-val cTyp_compdec : Structures.constr lazy_t
-val cunit_typ_compdec : Structures.constr lazy_t
-val cte_carrier : Structures.constr lazy_t
-val cte_compdec : Structures.constr lazy_t
-val ceqb_of_compdec : Structures.constr lazy_t
-val cCompDec : Structures.constr lazy_t
-
-val cbool_compdec : Structures.constr lazy_t
-val cZ_compdec : Structures.constr lazy_t
-val cPositive_compdec : Structures.constr lazy_t
-val cBV_compdec : Structures.constr lazy_t
-val cFArray_compdec : Structures.constr lazy_t
-
-val ctval : Structures.constr lazy_t
-val cTval : Structures.constr lazy_t
-
-val cCO_xH : Structures.constr lazy_t
-val cCO_Z0 : Structures.constr lazy_t
-val cCO_BV : Structures.constr lazy_t
-
-val cUO_xO : Structures.constr lazy_t
-val cUO_xI : Structures.constr lazy_t
-val cUO_Zpos : Structures.constr lazy_t
-val cUO_Zneg : Structures.constr lazy_t
-val cUO_Zopp : Structures.constr lazy_t
-val cUO_BVbitOf : Structures.constr lazy_t
-val cUO_BVnot : Structures.constr lazy_t
-val cUO_BVneg : Structures.constr lazy_t
-val cUO_BVextr : Structures.constr lazy_t
-val cUO_BVzextn : Structures.constr lazy_t
-val cUO_BVsextn : Structures.constr lazy_t
-
-val cBO_Zplus : Structures.constr lazy_t
-val cBO_Zminus : Structures.constr lazy_t
-val cBO_Zmult : Structures.constr lazy_t
-val cBO_Zlt : Structures.constr lazy_t
-val cBO_Zle : Structures.constr lazy_t
-val cBO_Zge : Structures.constr lazy_t
-val cBO_Zgt : Structures.constr lazy_t
-val cBO_eq : Structures.constr lazy_t
-val cBO_BVand : Structures.constr lazy_t
-val cBO_BVor : Structures.constr lazy_t
-val cBO_BVxor : Structures.constr lazy_t
-val cBO_BVadd : Structures.constr lazy_t
-val cBO_BVmult : Structures.constr lazy_t
-val cBO_BVult : Structures.constr lazy_t
-val cBO_BVslt : Structures.constr lazy_t
-val cBO_BVconcat : Structures.constr lazy_t
-val cBO_BVshl : Structures.constr lazy_t
-val cBO_BVshr : Structures.constr lazy_t
-val cBO_select : Structures.constr lazy_t
-val cBO_diffarray : Structures.constr lazy_t
-
-val cTO_store : Structures.constr lazy_t
-
-val cNO_distinct : Structures.constr lazy_t
-
-val catom : Structures.constr lazy_t
-val cAcop : Structures.constr lazy_t
-val cAuop : Structures.constr lazy_t
-val cAbop : Structures.constr lazy_t
-val cAtop : Structures.constr lazy_t
-val cAnop : Structures.constr lazy_t
-val cAapp : Structures.constr lazy_t
-
-val cform : Structures.constr lazy_t
-val cFatom : Structures.constr lazy_t
-val cFtrue : Structures.constr lazy_t
-val cFfalse : Structures.constr lazy_t
-val cFnot2 : Structures.constr lazy_t
-val cFand : Structures.constr lazy_t
-val cFor : Structures.constr lazy_t
-val cFxor : Structures.constr lazy_t
-val cFimp : Structures.constr lazy_t
-val cFiff : Structures.constr lazy_t
-val cFite : Structures.constr lazy_t
-val cFbbT : Structures.constr lazy_t
-
-val cis_true : Structures.constr lazy_t
-
-val cvalid_sat_checker : Structures.constr lazy_t
-val cinterp_var_sat_checker : Structures.constr lazy_t
+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 ->
-           Structures.constr array option ->
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t * Structures.constr lazy_t *
-           Structures.constr lazy_t * Structures.constr lazy_t
+           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
 
 (* Some constructions *)
-val ceq_refl_true : Structures.constr lazy_t
-val eq_refl_true : unit -> Structures.constr
-val vm_cast_true_no_check : Structures.constr -> Structures.constr
-val vm_cast_true : Environ.env -> Structures.constr -> Structures.constr
-val mkNat : int -> Structures.constr
-val mkN : int -> Structures.constr
-val mk_bv_list : bool list -> Structures.constr
+val ceq_refl_true : CoqInterface.constr lazy_t
+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
 
 (* Reification *)
-val mk_bool : Structures.constr -> bool
-val mk_bool_list : Structures.constr -> bool list
-val mk_nat : Structures.constr -> int
-val mk_N : Structures.constr -> int
-val mk_Z : Structures.constr -> int
-val mk_bvsize : Structures.constr -> int
+val mk_bool : CoqInterface.constr -> bool
+val mk_bool_list : CoqInterface.constr -> bool list
+val mk_nat : CoqInterface.constr -> int
+val mk_N : CoqInterface.constr -> int
+val mk_Z : CoqInterface.constr -> int
+val mk_bvsize : CoqInterface.constr -> int
 
 (* Switches between constr and OCaml *)
-val option_of_constr_option : Structures.constr -> Structures.constr option
-val list_of_constr_tuple : Structures.constr -> Structures.constr list
+val option_of_constr_option : CoqInterface.constr -> CoqInterface.constr option
+val list_of_constr_tuple : CoqInterface.constr -> CoqInterface.constr list
diff --git a/src/trace/satAtom.ml b/src/trace/satAtom.ml
index 6ffd752..0296c88 100644
--- a/src/trace/satAtom.ml
+++ b/src/trace/satAtom.ml
@@ -27,7 +27,7 @@ module Atom =
 
     type reify_tbl =
         { mutable count : int;
-	          tbl : (Structures.constr, int) Hashtbl.t
+	          tbl : (CoqInterface.constr, int) Hashtbl.t
 	}
 
     let create () = 
@@ -51,7 +51,7 @@ module Atom =
       t
 
     let interp_tbl reify =
-      Structures.mkArray (Lazy.force cbool, atom_tbl reify)
+      CoqInterface.mkArray (Lazy.force cbool, atom_tbl reify)
 
     let logic _ = SL.empty
 
diff --git a/src/trace/satAtom.mli b/src/trace/satAtom.mli
index b6a8dea..311b147 100644
--- a/src/trace/satAtom.mli
+++ b/src/trace/satAtom.mli
@@ -23,13 +23,13 @@ module Atom : sig
 
   type reify_tbl = {
       mutable count : int;
-      tbl : (Structures.constr, t) Hashtbl.t;
+      tbl : (CoqInterface.constr, t) Hashtbl.t;
     }
   val create : unit -> reify_tbl
-  val declare : reify_tbl -> Structures.constr -> t
-  val get : reify_tbl -> Structures.constr -> t
-  val atom_tbl : reify_tbl -> Structures.constr array
-  val interp_tbl : reify_tbl -> Structures.constr
+  val declare : reify_tbl -> CoqInterface.constr -> t
+  val get : reify_tbl -> CoqInterface.constr -> t
+  val atom_tbl : reify_tbl -> CoqInterface.constr array
+  val interp_tbl : reify_tbl -> CoqInterface.constr
 end
 
 
diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 2710eb2..78f2eee 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -85,7 +85,7 @@ type nop =
 type op_def = {
     tparams : SmtBtype.btype array;
     tres : SmtBtype.btype;
-    op_val : Structures.constr }
+    op_val : CoqInterface.constr }
 
 type index = Index of int
            | Rel_name of string
@@ -97,14 +97,14 @@ let destruct s (i, hval) = match i with
     | Rel_name _ -> failwith s
 
 let dummy_indexed_op i dom codom =
-  (i, {tparams = dom; tres = codom; op_val = Structures.mkProp})
+  (i, {tparams = dom; tres = codom; op_val = CoqInterface.mkProp})
 
 let indexed_op_index i =
   let index, _ = destruct "destruct on a Rel: called by indexed_op_index" i in
   index
 
 let debruijn_indexed_op i ty =
-  (Index i, {tparams = [||]; tres = ty; op_val = Structures.mkRel i})
+  (Index i, {tparams = [||]; tres = ty; op_val = CoqInterface.mkRel i})
 
 module Op =
   struct
@@ -357,7 +357,7 @@ module Op =
     (* reify table *)
     type reify_tbl =
       { mutable count : int;
-	        tbl : (Structures.constr, indexed_op) Hashtbl.t
+	        tbl : (CoqInterface.constr, indexed_op) Hashtbl.t
       }
 
     let create () =
@@ -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;
-      Structures.mkArray (tval, t)
+      CoqInterface.mkArray (tval, t)
 
     let to_list reify =
       let set _ op acc =
@@ -713,7 +713,7 @@ module Atom =
         to_smt_atom (atom h)
 
       and to_smt_atom = function
-        | Acop (CO_BV bv) -> if List.length bv = 0 then Structures.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv
+        | Acop (CO_BV bv) -> if List.length bv = 0 then CoqInterface.error "Empty bit-vectors are not valid in SMT" else Format.fprintf fmt "#b%a" bv_to_smt bv
         | Acop _ as a -> to_smt_int fmt (compute_int a)
         | Auop (op,h) -> to_smt_uop op h
         | Abop (op,h1,h2) -> to_smt_bop op h1 h2
@@ -740,7 +740,7 @@ module Atom =
         Array.iter (fun bt -> SmtBtype.to_smt fmt bt; Format.fprintf fmt " ") bta;
         Format.fprintf fmt ") ( ";
         SmtBtype.to_smt fmt bt;
-        Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (Structures.pr_constr t))
+        Format.fprintf fmt " ) ( %s )]" (Pp.string_of_ppcmds (CoqInterface.pr_constr t))
 
       and to_smt_uop op h =
         match op with
@@ -1107,8 +1107,8 @@ module Atom =
           else CCunknown_deps (gobble_of_coq_cst cc)
         with Not_found -> CCunknown
       in
-      let rec mk_hatom (h : Structures.constr) =
-        let c, args = Structures.decompose_app h in
+      let rec mk_hatom (h : CoqInterface.constr) =
+        let c, args = CoqInterface.decompose_app h in
 	match get_cst c with
         | CCxH -> mk_cop CCxH args
         | CCZ0 -> mk_cop CCZ0 args
@@ -1150,9 +1150,9 @@ module Atom =
         | CCselect -> mk_bop_select args
         | CCdiff -> mk_bop_diff args
         | CCstore -> mk_top_store args
-	| CCunknown -> mk_unknown c args (Structures.retyping_get_type_of env sigma h)
+	| CCunknown -> mk_unknown c args (CoqInterface.retyping_get_type_of env sigma h)
         | CCunknown_deps gobble ->
-          mk_unknown_deps c args (Structures.retyping_get_type_of env sigma h) gobble
+          mk_unknown_deps c args (CoqInterface.retyping_get_type_of env sigma h) gobble
 
 
       and mk_cop op args = match op, args with
@@ -1343,10 +1343,10 @@ module Atom =
         let rec collect_types = function
           | [] -> ([],[])
           | x::xs as l ->
-             let ty = Structures.retyping_get_type_of env sigma x in
+             let ty = CoqInterface.retyping_get_type_of env sigma x in
              if Constr.iskind ty ||
-                  let c, _ = Structures.decompose_app ty in
-                  Structures.eq_constr c (Lazy.force cCompDec)
+                  let c, _ = CoqInterface.decompose_app ty in
+                  CoqInterface.eq_constr c (Lazy.force cCompDec)
              then
                let (l1, l2) = collect_types xs in
                (x::l1, l2)
@@ -1365,10 +1365,10 @@ module Atom =
           with | Not_found ->
             let targs = Array.map type_of hargs in
             let tres = SmtBtype.of_coq rt known_logic ty in
-            let os = if Structures.isRel c then
-                       let i = Structures.destRel c in
-                       let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in
-                       Some (Structures.string_of_name n)
+            let os = if CoqInterface.isRel c then
+                       let i = CoqInterface.destRel c in
+                       let n, _ = CoqInterface.destruct_rel_decl (Environ.lookup_rel i env) in
+                       Some (CoqInterface.string_of_name n)
                      else if Vars.closed0 c then
                        None
                      else
@@ -1391,7 +1391,7 @@ module Atom =
          [gobble] *)
       and mk_unknown_deps c args ty gobble =
         let deps, args = split_list_at gobble args in
-        let c = Structures.mkApp (c, Array.of_list deps) in
+        let c = CoqInterface.mkApp (c, Array.of_list deps) in
         mk_unknown c args ty
 
       in
@@ -1432,7 +1432,7 @@ module Atom =
 
     let interp_tbl reify =
       let t = to_array reify (Lazy.force dft_atom) a_to_coq in
-      Structures.mkArray (Lazy.force catom, t)
+      CoqInterface.mkArray (Lazy.force catom, t)
 
 
     (** Producing a Coq term corresponding to the interpretation of an atom *)
@@ -1444,12 +1444,12 @@ module Atom =
 	  let pc =
 	    match atom a with
               | Acop c -> Op.interp_cop c
-              | Auop (op,h) -> Structures.mkApp (Op.interp_uop op, [|interp_atom h|])
+              | Auop (op,h) -> CoqInterface.mkApp (Op.interp_uop op, [|interp_atom h|])
               | Abop (op,h1,h2) ->
-                Structures.mkApp (Op.interp_bop t_i op,
+                CoqInterface.mkApp (Op.interp_bop t_i op,
                             [|interp_atom h1; interp_atom h2|])
               | Atop (op,h1,h2,h3) ->
-                Structures.mkApp (Op.interp_top t_i op,
+                CoqInterface.mkApp (Op.interp_top t_i op,
                             [|interp_atom h1; interp_atom h2; interp_atom h3|])
               | Anop (NO_distinct ty as op,ha) ->
                 let cop = Op.interp_nop t_i op in
@@ -1457,9 +1457,9 @@ module Atom =
                 let cargs = Array.fold_right (fun h l ->
                     mklApp ccons [|typ; interp_atom h; l|])
                     ha (mklApp cnil [|typ|]) in
-                Structures.mkApp (cop,[|cargs|])
+                CoqInterface.mkApp (cop,[|cargs|])
               | Aapp (op,t) ->
-                Structures.mkApp ((snd op).op_val, Array.map interp_atom t) in
+                CoqInterface.mkApp ((snd op).op_val, Array.map interp_atom t) in
 	  Hashtbl.add atom_tbl l pc;
 	  pc in
       interp_atom a
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index 645a638..27737ff 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -76,14 +76,14 @@ module Op :
 
     val create : unit -> reify_tbl
 
-    val declare : reify_tbl -> Structures.constr -> btype array ->
+    val declare : reify_tbl -> CoqInterface.constr -> btype array ->
                   btype -> string option -> indexed_op
 
-    val of_coq : reify_tbl -> Structures.constr -> indexed_op
+    val of_coq : reify_tbl -> CoqInterface.constr -> indexed_op
 
-    val interp_tbl : Structures.constr ->
-      (btype array -> btype -> Structures.constr -> Structures.constr) ->
-      reify_tbl -> Structures.constr
+    val interp_tbl : CoqInterface.constr ->
+      (btype array -> btype -> CoqInterface.constr -> CoqInterface.constr) ->
+      reify_tbl -> CoqInterface.constr
 
     val to_list : reify_tbl -> (int * (btype array) * btype * indexed_op) list
 
@@ -142,18 +142,18 @@ module Atom :
       (** Given a coq term, build the corresponding atom *)
       exception UnknownUnderForall
       val of_coq : ?eqsym:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
-        reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t
+        reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> CoqInterface.constr -> t
 
-      val get_coq_term_op : int -> Structures.constr
+      val get_coq_term_op : int -> CoqInterface.constr
 
-      val to_coq : t -> Structures.constr
+      val to_coq : t -> CoqInterface.constr
 
       val to_array : reify_tbl -> 'a -> (atom -> 'a) -> 'a array
 
-      val interp_tbl : reify_tbl -> Structures.constr
+      val interp_tbl : reify_tbl -> CoqInterface.constr
 
-      val interp_to_coq : Structures.constr -> (int, Structures.constr) Hashtbl.t ->
-	t -> Structures.constr
+      val interp_to_coq : CoqInterface.constr -> (int, CoqInterface.constr) Hashtbl.t ->
+	t -> CoqInterface.constr
 
       val logic : t -> SmtMisc.logic
 
@@ -201,5 +201,5 @@ module Trace : sig
 end
 
 
-val make_t_i : SmtBtype.reify_tbl -> Structures.constr
-val make_t_func : Op.reify_tbl -> Structures.constr -> Structures.constr
+val make_t_i : SmtBtype.reify_tbl -> CoqInterface.constr
+val make_t_func : Op.reify_tbl -> CoqInterface.constr -> CoqInterface.constr
diff --git a/src/trace/smtBtype.ml b/src/trace/smtBtype.ml
index 3b6d107..c9aad70 100644
--- a/src/trace/smtBtype.ml
+++ b/src/trace/smtBtype.ml
@@ -19,7 +19,7 @@ type uninterpreted_type =
   (* Uninterpreted type for which a CompDec is already known
      The constr is of type typ_compdec
    *)
-  | CompDec of Structures.constr
+  | CompDec of CoqInterface.constr
   (* Uninterpreted type for which the knowledge of a CompDec is delayed
      until either:
      - one is used
@@ -27,11 +27,11 @@ type uninterpreted_type =
        via a cut
      The constr is of type Type
    *)
-  | Delayed of Structures.constr
+  | Delayed of CoqInterface.constr
 
 type indexed_type = uninterpreted_type gen_hashed
 
-let dummy_indexed_type i = {index = i; hval = Delayed (Structures.mkProp)}
+let dummy_indexed_type i = {index = i; hval = Delayed (CoqInterface.mkProp)}
 let indexed_type_index i = i.index
 let indexed_type_compdec i =
   match i.hval with
@@ -105,8 +105,8 @@ let rec logic = function
 (* reify table *)
 type reify_tbl =
   { mutable count : int;
-    tbl : (Structures.constr, btype) Hashtbl.t;
-    mutable cuts : (Structures.id * Structures.types) list;
+    tbl : (CoqInterface.constr, btype) Hashtbl.t;
+    mutable cuts : (CoqInterface.id * CoqInterface.types) list;
     unsup_tbl : (btype, btype) Hashtbl.t;
   }
 
@@ -145,8 +145,8 @@ let interp_tbl reify =
             | CompDec compdec -> t.(it.index) <- compdec; Some bt
             | Delayed ty ->
                let n = string_of_int (List.length reify.cuts) in
-               let compdec_name = Structures.mkId ("CompDec"^n) in
-               let compdec_var = Structures.mkVar compdec_name in
+               let compdec_name = CoqInterface.mkId ("CompDec"^n) in
+               let compdec_var = CoqInterface.mkVar compdec_name in
                let compdec_type = mklApp cCompDec [| ty |] in
                reify.cuts <- (compdec_name, compdec_type) :: reify.cuts;
                let ce = mklApp cTyp_compdec [|ty; compdec_var|] in
@@ -156,7 +156,7 @@ let interp_tbl reify =
       | _ -> Some bt
   in
   Hashtbl.filter_map_inplace set reify.tbl;
-  Structures.mkArray (Lazy.force ctyp_compdec, t)
+  CoqInterface.mkArray (Lazy.force ctyp_compdec, t)
 
 
 let to_list reify =
@@ -241,8 +241,8 @@ let rec compdec_btype reify = function
   | Tindex i ->
      (match i.hval with
         | CompDec compdec ->
-           let c, args = Structures.decompose_app compdec in
-           if Structures.eq_constr c (Lazy.force cTyp_compdec) then
+           let c, args = CoqInterface.decompose_app compdec in
+           if CoqInterface.eq_constr c (Lazy.force cTyp_compdec) then
              match args with
                | [_; tic] -> tic
                | _ -> assert false
@@ -264,22 +264,22 @@ let declare_and_compdec reify t ty =
 
 let rec of_coq reify known_logic t =
   try
-    let c, args = Structures.decompose_app t in
-    if Structures.eq_constr c (Lazy.force cbool) ||
-         Structures.eq_constr c (Lazy.force cTbool) then Tbool
-    else if Structures.eq_constr c (Lazy.force cZ) ||
-              Structures.eq_constr c (Lazy.force cTZ) then
+    let c, args = CoqInterface.decompose_app t in
+    if CoqInterface.eq_constr c (Lazy.force cbool) ||
+         CoqInterface.eq_constr c (Lazy.force cTbool) then Tbool
+    else if CoqInterface.eq_constr c (Lazy.force cZ) ||
+              CoqInterface.eq_constr c (Lazy.force cTZ) then
       check_known TZ known_logic
-    else if Structures.eq_constr c (Lazy.force cpositive) ||
-              Structures.eq_constr c (Lazy.force cTpositive) then
+    else if CoqInterface.eq_constr c (Lazy.force cpositive) ||
+              CoqInterface.eq_constr c (Lazy.force cTpositive) then
       check_known Tpositive known_logic
-    else if Structures.eq_constr c (Lazy.force cbitvector) ||
-              Structures.eq_constr c (Lazy.force cTBV) then
+    else if CoqInterface.eq_constr c (Lazy.force cbitvector) ||
+              CoqInterface.eq_constr c (Lazy.force cTBV) then
       match args with
         | [s] -> check_known (TBV (mk_bvsize s)) known_logic
         | _ -> assert false
-    else if Structures.eq_constr c (Lazy.force cfarray) ||
-              Structures.eq_constr c (Lazy.force cTFArray) then
+    else if CoqInterface.eq_constr c (Lazy.force cfarray) ||
+              CoqInterface.eq_constr c (Lazy.force cTFArray) then
       match args with
         | ti :: te :: _ ->
            let ty = TFArray (of_coq reify known_logic ti,
diff --git a/src/trace/smtBtype.mli b/src/trace/smtBtype.mli
index ec73d21..7060ab6 100644
--- a/src/trace/smtBtype.mli
+++ b/src/trace/smtBtype.mli
@@ -17,7 +17,7 @@ type indexed_type
 
 val dummy_indexed_type: int -> indexed_type
 val indexed_type_index : indexed_type -> int
-val indexed_type_compdec : indexed_type -> Structures.constr
+val indexed_type_compdec : indexed_type -> CoqInterface.constr
 
 type btype =
   | TZ
@@ -31,7 +31,7 @@ val indexed_type_of_int : int -> indexed_type
 
 module HashedBtype : Hashtbl.HashedType with type t = btype
 
-val to_coq : btype -> Structures.constr
+val to_coq : btype -> CoqInterface.constr
 
 val to_smt : Format.formatter -> btype -> unit
 
@@ -40,25 +40,25 @@ type reify_tbl
 val create : unit -> reify_tbl
 val copy : reify_tbl -> reify_tbl
 
-val of_coq : reify_tbl -> logic -> Structures.constr -> btype
-val of_coq_compdec : reify_tbl -> Structures.constr -> Structures.constr -> btype
+val of_coq : reify_tbl -> logic -> CoqInterface.constr -> btype
+val of_coq_compdec : reify_tbl -> CoqInterface.constr -> CoqInterface.constr -> btype
 
-val get_coq_type_op : int -> Structures.constr
+val get_coq_type_op : int -> CoqInterface.constr
 
-val interp_tbl : reify_tbl -> Structures.constr
+val interp_tbl : reify_tbl -> CoqInterface.constr
 
 val to_list : reify_tbl ->  (int * indexed_type) list
 
-val make_t_i : reify_tbl -> Structures.constr
+val make_t_i : reify_tbl -> CoqInterface.constr
 
-val dec_interp : Structures.constr -> btype -> Structures.constr
-val ord_interp : Structures.constr -> btype -> Structures.constr
-val comp_interp : Structures.constr -> btype -> Structures.constr
-val inh_interp : Structures.constr -> btype -> Structures.constr
-val interp : Structures.constr -> btype -> Structures.constr
+val dec_interp : CoqInterface.constr -> btype -> CoqInterface.constr
+val ord_interp : CoqInterface.constr -> btype -> CoqInterface.constr
+val comp_interp : CoqInterface.constr -> btype -> CoqInterface.constr
+val inh_interp : CoqInterface.constr -> btype -> CoqInterface.constr
+val interp : CoqInterface.constr -> btype -> CoqInterface.constr
 
-val interp_to_coq : reify_tbl -> btype -> Structures.constr
+val interp_to_coq : reify_tbl -> btype -> CoqInterface.constr
 
-val get_cuts : reify_tbl -> (Structures.id * Structures.types) list
+val get_cuts : reify_tbl -> (CoqInterface.id * CoqInterface.types) list
 
 val logic : btype -> logic
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index 2ea4ca8..24cdf78 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -98,11 +98,11 @@ type 'hform rule =
     *)
 
   (* Linear arithmetic *)
-  | LiaMicromega of 'hform list * Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+  | LiaMicromega of 'hform list * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list
   | LiaDiseq of 'hform
 
   (* Arithmetic simplifications *)
-  | SplArith of 'hform clause * 'hform * Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+  | SplArith of 'hform clause * 'hform * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list
 
   (* Elimination of operators *)
   | SplDistinctElim of 'hform clause * 'hform
diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli
index 7da3097..bc2da38 100644
--- a/src/trace/smtCertif.mli
+++ b/src/trace/smtCertif.mli
@@ -96,11 +96,11 @@ type 'hform rule =
     *)
 
   (* Linear arithmetic *)
-  | LiaMicromega of 'hform list * Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+  | LiaMicromega of 'hform list * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list
   | LiaDiseq of 'hform
 
   (* Arithmetic simplifications *)
-  | SplArith of 'hform clause * 'hform * Structures.Micromega_plugin_Certificate.Mc.zArithProof list
+  | SplArith of 'hform clause * 'hform * CoqInterface.Micromega_plugin_Certificate.Mc.zArithProof list
 
   (* Elimination of operators *)
   | SplDistinctElim of 'hform clause * 'hform
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 =
diff --git a/src/trace/smtCommands.mli b/src/trace/smtCommands.mli
index b643594..e885028 100644
--- a/src/trace/smtCommands.mli
+++ b/src/trace/smtCommands.mli
@@ -11,13 +11,13 @@
 
 
 val parse_certif :
-  Structures.id ->
-  Structures.id ->
-  Structures.id ->
-  Structures.id ->
-  Structures.id ->
-  Structures.id ->
-  Structures.id ->
+  CoqInterface.id ->
+  CoqInterface.id ->
+  CoqInterface.id ->
+  CoqInterface.id ->
+  CoqInterface.id ->
+  CoqInterface.id ->
+  CoqInterface.id ->
   SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
   SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
   SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause ->
@@ -29,7 +29,7 @@ val checker_debug :
   SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause -> 'a
 
 val theorem :
-  Structures.id ->
+  CoqInterface.id ->
   SmtBtype.reify_tbl * SmtAtom.Op.reify_tbl *
   SmtAtom.Atom.reify_tbl * SmtAtom.Form.reify *
   SmtAtom.Form.t list * int * SmtAtom.Form.t SmtCertif.clause ->
@@ -56,8 +56,8 @@ val tactic :
   SmtAtom.Form.reify ->
   SmtAtom.Atom.reify_tbl ->
   SmtAtom.Form.reify ->
-  (Environ.env -> Structures.constr -> Structures.constr) ->
-  Structures.constr list ->
-  Structures.constr_expr list -> Structures.tactic
+  (Environ.env -> CoqInterface.constr -> CoqInterface.constr) ->
+  CoqInterface.constr list ->
+  CoqInterface.constr_expr list -> CoqInterface.tactic
 
 val model_string : Environ.env -> SmtBtype.reify_tbl -> 'a -> 'b -> 'c -> SExpr.t -> string
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 7f2ebd8..0a7d859 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -81,7 +81,7 @@ module type FORM =
     val get : ?declare:bool -> reify -> pform -> t
 
     (** Given a coq term, build the corresponding formula *)
-    val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t
+    val of_coq : (CoqInterface.constr -> hatom) -> reify -> CoqInterface.constr -> t
 
     val hash_hform : (hatom -> hatom) -> reify -> t -> t
     (* Flattening of [Fand] and [For], removing of [Fnot2]  *)
@@ -93,20 +93,20 @@ module type FORM =
 
     (** Producing Coq terms *)
 
-    val to_coq : t -> Structures.constr
+    val to_coq : t -> CoqInterface.constr
 
     val pform_tbl : reify -> pform array
 
     val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
-    val interp_tbl : reify -> Structures.constr * Structures.constr
+    val interp_tbl : reify -> CoqInterface.constr * CoqInterface.constr
     val nvars : reify -> int
     (* Producing a Coq term corresponding to the interpretation
        of a formula *)
     (* [interp_atom] map [hatom] to coq term, it is better if it produce
        shared terms. *)
     val interp_to_coq :
-      (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
-      t -> Structures.constr
+      (hatom -> CoqInterface.constr) -> (int, CoqInterface.constr) Hashtbl.t ->
+      t -> CoqInterface.constr
 
     (* Unstratified terms *)
     type atom_form_lit =
@@ -368,9 +368,9 @@ module Make (Atom:ATOM) =
       | CCunknown
 
     module ConstrHash = struct
-      type t = Structures.constr
-      let equal = Structures.eq_constr
-      let hash = Structures.hash_constr
+      type t = CoqInterface.constr
+      let equal = CoqInterface.eq_constr
+      let hash = CoqInterface.hash_constr
     end
     module ConstrHashtbl = Hashtbl.Make(ConstrHash)
 
@@ -393,7 +393,7 @@ module Make (Atom:ATOM) =
       let get_cst c =
         try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in
       let rec mk_hform h =
-        let c, args = Structures.decompose_app h in
+        let c, args = CoqInterface.decompose_app h in
         match get_cst c with
           | CCtrue  -> get reify (Fapp(Ftrue,empty_args))
           | CCfalse -> get reify (Fapp(Ffalse,empty_args))
@@ -408,7 +408,7 @@ module Make (Atom:ATOM) =
                    let l1 = mk_hform b1 in
                    let l2 = mk_hform b2 in
                    get reify (Fapp (Fimp, [|l1;l2|]))
-                | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb")
+                | _ -> CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments for implb")
           | CCifb ->
              (* We should also be able to reify if then else *)
              begin match args with
@@ -417,7 +417,7 @@ module Make (Atom:ATOM) =
                   let l2 = mk_hform b2 in
                   let l3 = mk_hform b3 in
                   get reify (Fapp (Fite, [|l1;l2;l3|]))
-               | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
+               | _ -> CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
              end
           | _ ->
              let a = atom_of_coq h in
@@ -429,13 +429,13 @@ module Make (Atom:ATOM) =
              let l1 = mk_hform b1 in
              let l2 = mk_hform b2 in
              get reify (f [|l1; l2|])
-          | _ ->  Structures.error "SmtForm.Form.of_coq: wrong number of arguments"
+          | _ ->  CoqInterface.error "SmtForm.Form.of_coq: wrong number of arguments"
 
       and mk_fnot i args =
         match args with
           | [t] ->
-             let c,args = Structures.decompose_app t in
-             if Structures.eq_constr c (Lazy.force cnegb) then
+             let c,args = CoqInterface.decompose_app t in
+             if CoqInterface.eq_constr c (Lazy.force cnegb) then
                mk_fnot (i+1) args
              else
                let q,r = i lsr 1 , i land 1 in
@@ -443,31 +443,31 @@ module Make (Atom:ATOM) =
                let l = if r = 0 then l else neg l in
                if q = 0 then l
                else get reify (Fapp(Fnot2 q, [|l|]))
-          | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
+          | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
 
       and mk_fand acc args =
         match args with
           | [t1;t2] ->
              let l2 = mk_hform t2 in
-             let c, args = Structures.decompose_app t1 in
-             if Structures.eq_constr c (Lazy.force candb) then
+             let c, args = CoqInterface.decompose_app t1 in
+             if CoqInterface.eq_constr c (Lazy.force candb) then
                mk_fand (l2::acc) args
              else
                let l1 = mk_hform t1 in
                get reify (Fapp(Fand, Array.of_list (l1::l2::acc)))
-          | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb"
+          | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for andb"
 
       and mk_for acc args =
         match args with
           | [t1;t2] ->
              let l2 = mk_hform t2 in
-             let c, args = Structures.decompose_app t1 in
-             if Structures.eq_constr c (Lazy.force corb) then
+             let c, args = CoqInterface.decompose_app t1 in
+             if CoqInterface.eq_constr c (Lazy.force corb) then
                mk_for (l2::acc) args
              else
                let l1 = mk_hform t1 in
                get reify (Fapp(For, Array.of_list (l1::l2::acc)))
-          | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
+          | _ -> CoqInterface.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
 
       mk_hform c
 
@@ -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;
-      Structures.mkArray (Lazy.force cint, cargs)
+      CoqInterface.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, Structures.mkArray (Lazy.force cform, t))
+      (mkInt i, CoqInterface.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/smtForm.mli b/src/trace/smtForm.mli
index 06a867f..47b4123 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -77,7 +77,7 @@ module type FORM =
       val get : ?declare:bool -> reify -> pform -> t
 
       (** Given a coq term, build the corresponding formula *)
-      val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t
+      val of_coq : (CoqInterface.constr -> hatom) -> reify -> CoqInterface.constr -> t
 
       val hash_hform : (hatom -> hatom) -> reify -> t -> t
 
@@ -90,20 +90,20 @@ module type FORM =
 
       (** Producing Coq terms *)
 
-      val to_coq : t -> Structures.constr
+      val to_coq : t -> CoqInterface.constr
 
       val pform_tbl : reify -> pform array
 
       val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
-      val interp_tbl : reify -> Structures.constr * Structures.constr
+      val interp_tbl : reify -> CoqInterface.constr * CoqInterface.constr
       val nvars : reify -> int
       (* Producing a Coq term corresponding to the interpretation
          of a formula *)
       (* [interp_atom] map [hatom] to coq term, it is better if it produce
          shared terms. *)
       val interp_to_coq :
-	  (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
-	    t -> Structures.constr
+	  (hatom -> CoqInterface.constr) -> (int, CoqInterface.constr) Hashtbl.t ->
+	    t -> CoqInterface.constr
 
       (* Unstratified terms *)
       type atom_form_lit =
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index d750550..165814b 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -16,7 +16,7 @@ let cInt_tbl = Hashtbl.create 17
 let mkInt i = 
   try Hashtbl.find cInt_tbl i 
   with Not_found ->
-    let ci = Structures.mkInt i in
+    let ci = CoqInterface.mkInt i in
     Hashtbl.add cInt_tbl i ci;
     ci
 
@@ -25,15 +25,15 @@ type 'a gen_hashed = { index : int; hval : 'a }
 
 
 (** Functions over constr *)
-let mklApp f args = Structures.mkApp (Lazy.force f, args)
+let mklApp f args = CoqInterface.mkApp (Lazy.force f, args)
 
-let string_of_name_def d n = try Structures.string_of_name n with | _ -> d
+let string_of_name_def d n = try CoqInterface.string_of_name n with | _ -> d
 
 let string_coq_constr t =
   let rec fix rf x = rf (fix rf) x in
   let pr = fix
-      Ppconstr.modular_constr_pr Pp.mt Structures.ppconstr_lsimpleconstr in
-  Pp.string_of_ppcmds (pr (Structures.constrextern_extern_constr t))
+      Ppconstr.modular_constr_pr Pp.mt CoqInterface.ppconstr_lsimpleconstr in
+  Pp.string_of_ppcmds (pr (CoqInterface.constrextern_extern_constr t))
 
 
 (** Logics *)
diff --git a/src/trace/smtMisc.mli b/src/trace/smtMisc.mli
index a6f5db8..5359c15 100644
--- a/src/trace/smtMisc.mli
+++ b/src/trace/smtMisc.mli
@@ -10,12 +10,12 @@
 (**************************************************************************)
 
 
-val cInt_tbl : (int, Structures.constr) Hashtbl.t
-val mkInt : int -> Structures.constr
+val cInt_tbl : (int, CoqInterface.constr) Hashtbl.t
+val mkInt : int -> CoqInterface.constr
 type 'a gen_hashed = { index : int; hval : 'a; }
-val mklApp : Structures.constr Lazy.t -> Structures.constr array -> Structures.constr
-val string_of_name_def : string -> Structures.name -> string
-val string_coq_constr : Structures.constr -> string
+val mklApp : CoqInterface.constr Lazy.t -> CoqInterface.constr array -> CoqInterface.constr
+val string_of_name_def : string -> CoqInterface.name -> string
+val string_coq_constr : CoqInterface.constr -> string
 type logic_item = LUF | LLia | LBitvectors | LArrays
 module SL : Set.S with type elt = logic_item
 type logic = SL.t
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 65994f9..7b68a26 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); Structures.mkArray (Lazy.force cint, args)|]
+	mklApp cRes [|mkInt (get_pos c); CoqInterface.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 Structures.micromega_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Structures.micromega_coq_proofTerm|]) 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
           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_coq_proofTerm; Structures.micromega_dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Structures.micromega_coq_proofTerm|]) 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
           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|]
@@ -461,10 +461,10 @@ let to_coq to_lit interp (cstep,
         | Ext (res) -> mklApp cExt [|out_c c; out_f res|]
         | Hole (prem_id, concl) ->
            let prem = List.map (fun cl -> match cl.value with Some l -> l | None -> assert false) prem_id in
-           let ass_name = Structures.mkId ("ass"^(string_of_int (Hashtbl.hash concl))) in
+           let ass_name = CoqInterface.mkId ("ass"^(string_of_int (Hashtbl.hash concl))) in
            let ass_ty = interp (prem, concl) in
            cuts := (ass_name, ass_ty)::!cuts;
-           let ass_var = Structures.mkVar ass_name in
+           let ass_var = CoqInterface.mkVar ass_name in
            let prem_id' = List.fold_right (fun c l -> mklApp ccons [|Lazy.force cint; out_c c; l|]) prem_id (mklApp cnil [|Lazy.force cint|]) in
            let prem' = List.fold_right (fun cl l -> mklApp ccons [|Lazy.force cState_C_t; out_cl cl; l|]) prem (mklApp cnil [|Lazy.force cState_C_t|]) in
            let concl' = out_cl concl in
@@ -474,23 +474,23 @@ let to_coq to_lit interp (cstep,
              | Some find -> find cl
              | None -> assert false in
            let concl' = out_cl [concl] in
-           let app_name = Structures.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in
-           let app_var = Structures.mkVar app_name in
-           let app_ty = Structures.mkArrow clemma (interp ([], [concl])) in
+           let app_name = CoqInterface.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in
+           let app_var = CoqInterface.mkVar app_name in
+           let app_ty = CoqInterface.mkArrow clemma (interp ([], [concl])) in
            cuts := (app_name, app_ty)::!cuts;
            mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|]
 	end
     | _ -> assert false in
   let step = Lazy.force cstep in
   let def_step =
-    mklApp cRes [|mkInt 0; Structures.mkArray (Lazy.force cint, [|mkInt 0|]) |] in
+    mklApp cRes [|mkInt 0; CoqInterface.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;
   let last_root = !r in
   (* Be careful, step_to_coq makes a side effect on cuts so it needs to be called first *)
   let res =
-    Structures.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r
+    CoqInterface.mkTrace step_to_coq next carray clist cnil ccons cpair !nc step def_step r
   in
   (res, last_root, !cuts)
 
diff --git a/src/trace/smtTrace.mli b/src/trace/smtTrace.mli
index 2c70bbc..e79ce20 100644
--- a/src/trace/smtTrace.mli
+++ b/src/trace/smtTrace.mli
@@ -48,26 +48,26 @@ val alloc : 'a SmtCertif.clause -> int
 val naive_alloc : 'a SmtCertif.clause -> int
 val build_certif : 'a SmtCertif.clause -> 'b SmtCertif.clause -> int
 val to_coq :
-  ('a -> Structures.constr) ->
-  ('a list list * 'a list -> Structures.types) ->
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t * Structures.constr Lazy.t *
-  Structures.constr Lazy.t * Structures.constr Lazy.t ->
+  ('a -> CoqInterface.constr) ->
+  ('a list list * 'a list -> CoqInterface.types) ->
+  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 ->
   'a SmtCertif.clause ->
-  ('a SmtCertif.clause -> Structures.types * Structures.constr) option ->
-  Structures.constr * 'a SmtCertif.clause *
-    (Structures.id * Structures.types) list
+  ('a SmtCertif.clause -> CoqInterface.types * CoqInterface.constr) option ->
+  CoqInterface.constr * 'a SmtCertif.clause *
+    (CoqInterface.id * CoqInterface.types) list
 
 
 module MakeOpt :
diff --git a/src/verit/verit.ml b/src/verit/verit.ml
index eed1dca..7f89943 100644
--- a/src/verit/verit.ml
+++ b/src/verit/verit.ml
@@ -193,25 +193,25 @@ let call_verit _ rt ro ra_quant rf_quant first lsmt =
         if l = "warning : proof_done: status is still open" then
           raise Unknown
         else if l = "Invalid memory reference" then
-          Structures.warning "verit-warning" ("veriT outputted the warning: " ^ l)
+          CoqInterface.warning "verit-warning" ("veriT outputted the warning: " ^ l)
         else if n >= 7 && String.sub l 0 7 = "warning" then
-          Structures.warning "verit-warning" ("veriT outputted the warning: " ^ (String.sub l 7 (n-7)))
+          CoqInterface.warning "verit-warning" ("veriT outputted the warning: " ^ (String.sub l 7 (n-7)))
         else if n >= 8 && String.sub l 0 8 = "error : " then
-          Structures.error ("veriT failed with the error: " ^ (String.sub l 8 (n-8)))
+          CoqInterface.error ("veriT failed with the error: " ^ (String.sub l 8 (n-8)))
         else
-          Structures.error ("veriT failed with the error: " ^ l)
+          CoqInterface.error ("veriT failed with the error: " ^ l)
       done
     with End_of_file -> () in
 
   try
-    if exit_code <> 0 then Structures.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code);
+    if exit_code <> 0 then CoqInterface.warning "verit-non-zero-exit-code" ("Verit.call_verit: command " ^ command ^ " exited with code " ^ string_of_int exit_code);
     raise_warnings_errors ();
     let res = import_trace ra_quant rf_quant logfilename (Some first) lsmt in
     close_in win; Sys.remove wname; res
   with x -> close_in win; Sys.remove wname;
             match x with
-            | Unknown -> Structures.error "veriT returns 'unknown'"
-            | VeritSyntax.Sat -> Structures.error "veriT found a counter-example"
+            | Unknown -> CoqInterface.error "veriT returns 'unknown'"
+            | VeritSyntax.Sat -> CoqInterface.error "veriT found a counter-example"
             | _ -> raise x
 
 let verit_logic =
diff --git a/src/verit/verit.mli b/src/verit/verit.mli
index 0560d77..f0acd0c 100644
--- a/src/verit/verit.mli
+++ b/src/verit/verit.mli
@@ -11,13 +11,13 @@
 
 
 val parse_certif :
-  Structures.id ->
-  Structures.id ->
-  Structures.id ->
-  Structures.id ->
-  Structures.id -> Structures.id -> Structures.id -> string -> string -> unit
+  CoqInterface.id ->
+  CoqInterface.id ->
+  CoqInterface.id ->
+  CoqInterface.id ->
+  CoqInterface.id -> CoqInterface.id -> CoqInterface.id -> string -> string -> unit
 val checker : string -> string -> unit
 val checker_debug : string -> string -> unit
-val theorem : Structures.id -> string -> string -> unit
-val tactic : EConstr.t -> Structures.constr_expr list -> Structures.tactic
-val tactic_no_check : EConstr.t -> Structures.constr_expr list -> Structures.tactic
+val theorem : CoqInterface.id -> string -> string -> unit
+val tactic : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
+val tactic_no_check : EConstr.t -> CoqInterface.constr_expr list -> CoqInterface.tactic
diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index 21c10e8..c5db594 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -493,7 +493,7 @@ let mk_clause (id,typ,value,ids_params) =
 let mk_clause cl =
   try mk_clause cl
   with Failure f ->
-    Structures.error ("SMTCoq was not able to check the certificate \
+    CoqInterface.error ("SMTCoq was not able to check the certificate \
                        for the following reason.\n"^f)
 
 let apply_dec f (decl, a) = decl, f a
diff --git a/src/versions/native/Make b/src/versions/native/Make
deleted file mode 100644
index e278c82..0000000
--- a/src/versions/native/Make
+++ /dev/null
@@ -1,171 +0,0 @@
-########################################################################
-##   This file is intended to developers, please do not use it to     ##
-## generate a Makefile, rather use the provided Makefile.             ##
-########################################################################
-
-
-
-
-########################################################################
-## To generate the Makefile:                                          ##
-##   coq_makefile -f Make -o Makefile                                 ##
-## In the Makefile :                                                  ##
-## 1) Suppress the "Makefile" target                                  ##
-## 2) Change the "all" target into:                                   ##
-##    all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES)                  ##
-## 3) Change the "install-natdynlink" target:                         ##
-##    change CMXSFILES into CMXS and add the same block for CMXA and VCMXS. ##
-## 4) Change the "install" target: change CMOFILES into CMXFILES.     ##
-## 5) Add to the "clean" target:                                      ##
-##    - rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.mli ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a ##
-########################################################################
-
-
--R . SMTCoq
-
--I bva
--I classes
--I array
--I cnf
--I euf
--I lfsc
--I lia
--I smtlib2
--I trace
--I verit
--I zchaff
--I versions/native
--I ../3rdparty/alt-ergo
-
-
--custom "cd ../unit-tests; make vernac" "" "test"
--custom "cd ../unit-tests; make zchaffv" "" "ztest"
--custom "cd ../unit-tests; make veritv" "" "vtest"
-
--custom "$(CAMLLEX) $<" "%.mll" "%.ml"
--custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
--custom "" "verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml" "ml"
-
--custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx trace/smtMaps.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx" "$(CMXA)"
--custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
-
-CMXA = smtcoq.cmxa
-CMXS = smtcoq_plugin.cmxs
-VCMXS = "versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs classes/NSMTCoq_SMT_classes.cmxs classes/NSMTCoq_SMT_classes_instances.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_Tactics.cmxs NSMTCoq_Conversion_tactics.cmxs NSMTCoq_PropToBool.cmxs NSMTCoq_BoolToProp.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi classes/NSMTCoq_SMT_classes.cmi classes/NSMTCoq_SMT_classes_instances.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_Tactics.cmi NSMTCoq_Conversion_tactics.cmi NSMTCoq_PropToBool.cmi NSMTCoq_BoolToProp.cmi NSMTCoq_SMTCoq.cmi"
-CAMLLEX = $(CAMLBIN)ocamllex
-CAMLYACC = $(CAMLBIN)ocamlyacc
-
-bva/BVList.v
-bva/Bva_checker.v
-
-classes/SMT_classes.v
-classes/SMT_classes_instances.v
-
-array/FArray.v
-array/Array_checker.v
-
-versions/native/Structures.v
-versions/native/structures.ml
-versions/native/structures.mli
-
-trace/coqTerms.ml
-trace/coqTerms.mli
-trace/satAtom.ml
-trace/satAtom.mli
-trace/smtAtom.ml
-trace/smtAtom.mli
-trace/smtBtype.ml
-trace/smtBtype.mli
-trace/smtCertif.ml
-trace/smtCertif.mli
-trace/smtCnf.ml
-trace/smtCnf.mli
-trace/smtCommands.ml
-trace/smtCommands.mli
-trace/smtForm.ml
-trace/smtForm.mli
-trace/smtMaps.ml
-trace/smtMaps.mli
-trace/smtMisc.ml
-trace/smtMisc.mli
-trace/smtTrace.ml
-trace/smtTrace.mli
-
-../3rdparty/alt-ergo/smtlib2_parse.ml
-../3rdparty/alt-ergo/smtlib2_parse.mli
-../3rdparty/alt-ergo/smtlib2_lex.ml
-../3rdparty/alt-ergo/smtlib2_lex.mli
-../3rdparty/alt-ergo/smtlib2_ast.ml
-../3rdparty/alt-ergo/smtlib2_ast.mli
-../3rdparty/alt-ergo/smtlib2_util.ml
-../3rdparty/alt-ergo/smtlib2_util.mli
-
-smtlib2/smtlib2_genConstr.ml
-smtlib2/smtlib2_genConstr.mli
-smtlib2/sExprParser.ml
-smtlib2/sExprParser.mli
-smtlib2/sExprLexer.ml
-smtlib2/sExpr.ml
-smtlib2/sExpr.mli
-smtlib2/smtlib2_solver.ml
-smtlib2/smtlib2_solver.mli
-
-verit/veritParser.ml
-verit/veritParser.mli
-verit/veritLexer.ml
-verit/veritLexer.mli
-verit/verit.ml
-verit/verit.mli
-verit/veritSyntax.ml
-verit/veritSyntax.mli
-
-lfsc/shashcons.mli
-lfsc/shashcons.ml
-lfsc/hstring.mli
-lfsc/hstring.ml
-lfsc/lfscParser.ml
-lfsc/lfscLexer.ml
-lfsc/type.ml
-lfsc/ast.ml
-lfsc/ast.mli
-lfsc/translator_sig.mli
-lfsc/builtin.ml
-lfsc/tosmtcoq.ml
-lfsc/tosmtcoq.mli
-lfsc/converter.ml
-lfsc/lfsc.ml
-
-zchaff/cnfParser.ml
-zchaff/cnfParser.mli
-zchaff/satParser.ml
-zchaff/satParser.mli
-zchaff/zchaff.ml
-zchaff/zchaff.mli
-zchaff/zchaffParser.ml
-zchaff/zchaffParser.mli
-
-cnf/Cnf.v
-
-euf/Euf.v
-
-lia/lia.ml
-lia/lia.mli
-lia/Lia.v
-
-spl/Assumptions.v
-spl/Syntactic.v
-spl/Arithmetic.v
-spl/Operators.v
-
-Conversion_tactics.v
-Misc.v
-SMTCoq.v
-ReflectFacts.v
-PropToBool.v
-BoolToProp.v
-Tactics.v
-SMT_terms.v
-State.v
-Trace.v
-
-smtcoq_plugin.ml4
diff --git a/src/versions/native/Makefile b/src/versions/native/Makefile
deleted file mode 100644
index aaaab9e..0000000
--- a/src/versions/native/Makefile
+++ /dev/null
@@ -1,505 +0,0 @@
-#############################################################################
-##  v      #                   The Coq Proof Assistant                     ##
-## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
-##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile Vtrunk      ##
-#############################################################################
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
-#
-# This Makefile was generated by the command line :
-# coq_makefile -f Make -o Makefile 
-#
-
-.DEFAULT_GOAL := all
-
-# 
-# This Makefile may take arguments passed as environment variables:
-# COQBIN to specify the directory where Coq binaries resides;
-# ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
-# DSTROOT to specify a prefix to install path.
-
-# Here is a hack to make $(eval $(shell works:
-define donewline
-
-
-endef
-includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr '\n' '@'; })))
-$(call includecmdwithout@,$(COQBIN)coqtop -config)
-
-##########################
-#                        #
-# Libraries definitions. #
-#                        #
-##########################
-
-OCAMLLIBS?=-I ../3rdparty/alt-ergo\
-  -I versions/native\
-  -I zchaff\
-  -I verit\
-  -I trace\
-  -I smtlib2\
-  -I lia\
-  -I lfsc\
-  -I euf\
-  -I cnf\
-  -I array\
-  -I classes\
-  -I bva
-COQLIBS?=-I ../3rdparty/alt-ergo\
-  -I versions/native\
-  -I zchaff\
-  -I verit\
-  -I trace\
-  -I smtlib2\
-  -I lia\
-  -I lfsc\
-  -I euf\
-  -I cnf\
-  -I array\
-  -I classes\
-  -I bva -R . SMTCoq
-COQDOCLIBS?=-R . SMTCoq
-
-##########################
-#                        #
-# Variables definitions. #
-#                        #
-##########################
-
-CAMLYACC=$(CAMLBIN)ocamlyacc
-CAMLLEX=$(CAMLBIN)ocamllex
-VCMXS=versions/native/NSMTCoq_versions_native_Structures.cmxs NSMTCoq_State.cmxs NSMTCoq_Misc.cmxs classes/NSMTCoq_SMT_classes.cmxs classes/NSMTCoq_SMT_classes_instances.cmxs NSMTCoq_SMT_terms.cmxs cnf/NSMTCoq_cnf_Cnf.cmxs euf/NSMTCoq_euf_Euf.cmxs lia/NSMTCoq_lia_Lia.cmxs spl/NSMTCoq_spl_Syntactic.cmxs spl/NSMTCoq_spl_Assumptions.cmxs spl/NSMTCoq_spl_Arithmetic.cmxs spl/NSMTCoq_spl_Operators.cmxs NSMTCoq_Trace.cmxs NSMTCoq_Tactics.cmxs NSMTCoq_Conversion_tactics.cmxs NSMTCoq_PropToBool.cmxs NSMTCoq_BoolToProp.cmxs NSMTCoq_SMTCoq.cmxs NSMTCoq_State.cmi NSMTCoq_Misc.cmi classes/NSMTCoq_SMT_classes.cmi classes/NSMTCoq_SMT_classes_instances.cmi NSMTCoq_SMT_terms.cmi cnf/NSMTCoq_cnf_Cnf.cmi euf/NSMTCoq_euf_Euf.cmi lia/NSMTCoq_lia_Lia.cmi spl/NSMTCoq_spl_Syntactic.cmi spl/NSMTCoq_spl_Assumptions.cmi spl/NSMTCoq_spl_Arithmetic.cmi spl/NSMTCoq_spl_Operators.cmi NSMTCoq_Trace.cmi NSMTCoq_Trace.cmi NSMTCoq_Tactics.cmi NSMTCoq_Conversion_tactics.cmi NSMTCoq_PropToBool.cmi NSMTCoq_BoolToProp.cmi NSMTCoq_SMTCoq.cmi
-CMXS=smtcoq_plugin.cmxs
-CMXA=smtcoq.cmxa
-
-OPT?=
-COQDEP?=$(COQBIN)coqdep -c
-COQFLAGS?=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)
-COQCHKFLAGS?=-silent -o
-COQDOCFLAGS?=-interpolate -utf8
-COQC?=$(COQBIN)coqc
-GALLINA?=$(COQBIN)gallina
-COQDOC?=$(COQBIN)coqdoc
-COQCHK?=$(COQBIN)coqchk
-
-COQSRCLIBS?=-I $(COQLIB)kernel -I $(COQLIB)lib \
-  -I $(COQLIB)library -I $(COQLIB)parsing \
-  -I $(COQLIB)pretyping -I $(COQLIB)interp \
-  -I $(COQLIB)proofs -I $(COQLIB)tactics \
-  -I $(COQLIB)toplevel \
-  -I $(COQLIB)plugins/btauto \
-  -I $(COQLIB)plugins/cc \
-  -I $(COQLIB)plugins/decl_mode \
-  -I $(COQLIB)plugins/extraction \
-  -I $(COQLIB)plugins/field \
-  -I $(COQLIB)plugins/firstorder \
-  -I $(COQLIB)plugins/fourier \
-  -I $(COQLIB)plugins/funind \
-  -I $(COQLIB)plugins/micromega \
-  -I $(COQLIB)plugins/nsatz \
-  -I $(COQLIB)plugins/omega \
-  -I $(COQLIB)plugins/quote \
-  -I $(COQLIB)plugins/ring \
-  -I $(COQLIB)plugins/romega \
-  -I $(COQLIB)plugins/rtauto \
-  -I $(COQLIB)plugins/setoid_ring \
-  -I $(COQLIB)plugins/syntax \
-  -I $(COQLIB)plugins/xml
-ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
-
-CAMLC?=$(OCAMLC) -c -rectypes
-CAMLOPTC?=$(OCAMLOPT) -c -rectypes
-CAMLLINK?=$(OCAMLC) -rectypes
-CAMLOPTLINK?=$(OCAMLOPT) -rectypes
-GRAMMARS?=grammar.cma
-CAMLP4EXTEND?=pa_extend.cmo pa_macro.cmo q_MLast.cmo
-CAMLP4OPTIONS?=-loc loc
-PP?=-pp "$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl"
-
-##################
-#                #
-# Install Paths. #
-#                #
-##################
-
-ifdef USERINSTALL
-XDG_DATA_HOME?=$(HOME)/.local/share
-COQLIBINSTALL=$(XDG_DATA_HOME)/coq
-COQDOCINSTALL=$(XDG_DATA_HOME)/doc/coq
-else
-COQLIBINSTALL=${COQLIB}user-contrib
-COQDOCINSTALL=${DOCDIR}user-contrib
-endif
-
-######################
-#                    #
-# Files dispatching. #
-#                    #
-######################
-
-VFILES:=Trace.v\
-  State.v\
-  SMT_terms.v\
-  Tactics.v\
-  BoolToProp.v\
-  PropToBool.v\
-  ReflectFacts.v\
-  SMTCoq.v\
-  Misc.v\
-  Conversion_tactics.v\
-  spl/Operators.v\
-  spl/Arithmetic.v\
-  spl/Syntactic.v\
-  spl/Assumptions.v\
-  lia/Lia.v\
-  euf/Euf.v\
-  cnf/Cnf.v\
-  versions/native/Structures.v\
-  array/Array_checker.v\
-  array/FArray.v\
-  classes/SMT_classes_instances.v\
-  classes/SMT_classes.v\
-  bva/Bva_checker.v\
-  bva/BVList.v
-
--include $(addsuffix .d,$(VFILES))
-.SECONDARY: $(addsuffix .d,$(VFILES))
-
-vo_to_obj = $(addsuffix .o,$(foreach vo,$(1),$(addprefix $(dir $(vo)),$(filter-out Warning: Error:,$(firstword $(shell $(COQBIN)coqtop -batch -quiet -print-mod-uid $(vo:.vo=)))))))
-VOFILES:=$(foreach vo,$(VFILES:.v=.vo),$(dir $(vo))$(notdir $(vo)))
-GLOBFILES:=$(VFILES:.v=.glob)
-VIFILES:=$(VFILES:.v=.vi)
-GFILES:=$(VFILES:.v=.g)
-HTMLFILES:=$(VFILES:.v=.html)
-GHTMLFILES:=$(VFILES:.v=.g.html)
-OBJFILES:=$(call vo_to_obj,$(VOFILES))
-ML4FILES:=smtcoq_plugin.ml4
-
--include $(addsuffix .d,$(ML4FILES))
-.SECONDARY: $(addsuffix .d,$(ML4FILES))
-
-MLFILES:=lia/lia.ml\
-  zchaff/zchaffParser.ml\
-  zchaff/zchaff.ml\
-  zchaff/satParser.ml\
-  zchaff/cnfParser.ml\
-  lfsc/lfsc.ml\
-  lfsc/converter.ml\
-  lfsc/tosmtcoq.ml\
-  lfsc/builtin.ml\
-  lfsc/ast.ml\
-  lfsc/type.ml\
-  lfsc/lfscLexer.ml\
-  lfsc/lfscParser.ml\
-  lfsc/hstring.ml\
-  lfsc/shashcons.ml\
-  verit/veritSyntax.ml\
-  verit/verit.ml\
-  verit/veritLexer.ml\
-  verit/veritParser.ml\
-  smtlib2/smtlib2_solver.ml\
-  smtlib2/sExpr.ml\
-  smtlib2/sExprLexer.ml\
-  smtlib2/sExprParser.ml\
-  smtlib2/smtlib2_genConstr.ml\
-  ../3rdparty/alt-ergo/smtlib2_util.ml\
-  ../3rdparty/alt-ergo/smtlib2_ast.ml\
-  ../3rdparty/alt-ergo/smtlib2_lex.ml\
-  ../3rdparty/alt-ergo/smtlib2_parse.ml\
-  trace/smtTrace.ml\
-  trace/smtMisc.ml\
-  trace/smtMaps.ml\
-  trace/smtForm.ml\
-  trace/smtCommands.ml\
-  trace/smtCnf.ml\
-  trace/smtCertif.ml\
-  trace/smtBtype.ml\
-  trace/smtAtom.ml\
-  trace/satAtom.ml\
-  trace/coqTerms.ml\
-  versions/native/structures.ml
-
--include $(addsuffix .d,$(MLFILES))
-.SECONDARY: $(addsuffix .d,$(MLFILES))
-
-MLIFILES:=lia/lia.mli\
-  zchaff/zchaffParser.mli\
-  zchaff/zchaff.mli\
-  zchaff/satParser.mli\
-  zchaff/cnfParser.mli\
-  lfsc/tosmtcoq.mli\
-  lfsc/translator_sig.mli\
-  lfsc/ast.mli\
-  lfsc/hstring.mli\
-  lfsc/shashcons.mli\
-  verit/veritSyntax.mli\
-  verit/verit.mli\
-  verit/veritLexer.mli\
-  verit/veritParser.mli\
-  smtlib2/smtlib2_solver.mli\
-  smtlib2/sExpr.mli\
-  smtlib2/sExprParser.mli\
-  smtlib2/smtlib2_genConstr.mli\
-  ../3rdparty/alt-ergo/smtlib2_util.mli\
-  ../3rdparty/alt-ergo/smtlib2_ast.mli\
-  ../3rdparty/alt-ergo/smtlib2_lex.mli\
-  ../3rdparty/alt-ergo/smtlib2_parse.mli\
-  trace/smtTrace.mli\
-  trace/smtMisc.mli\
-  trace/smtMaps.mli\
-  trace/smtForm.mli\
-  trace/smtCommands.mli\
-  trace/smtCnf.mli\
-  trace/smtCertif.mli\
-  trace/smtBtype.mli\
-  trace/smtAtom.mli\
-  trace/satAtom.mli\
-  trace/coqTerms.mli\
-  versions/native/structures.mli
-
--include $(addsuffix .d,$(MLIFILES))
-.SECONDARY: $(addsuffix .d,$(MLIFILES))
-
-ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)
-CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))
-CMXFILES=$(CMOFILES:.cmo=.cmx)
-CMIFILES=$(sort $(ALLCMOFILES:.cmo=.cmi) $(MLIFILES:.mli=.cmi))
-CMXSFILES=$(CMXFILES:.cmx=.cmxs)
-
-#######################################
-#                                     #
-# Definition of the toplevel targets. #
-#                                     #
-#######################################
-
-all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES)
-
-mlihtml: $(MLIFILES:.mli=.cmi)
-	 mkdir $@ || rm -rf $@/*
-	$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
-
-all-mli.tex: $(MLIFILES:.mli=.cmi)
-	$(OCAMLDOC) -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
-
-spec: $(VIFILES)
-
-gallina: $(GFILES)
-
-html: $(GLOBFILES) $(VFILES)
-	- mkdir -p html
-	$(COQDOC) -toc $(COQDOCFLAGS) -html $(COQDOCLIBS) -d html $(VFILES)
-
-gallinahtml: $(GLOBFILES) $(VFILES)
-	- mkdir -p html
-	$(COQDOC) -toc $(COQDOCFLAGS) -html -g $(COQDOCLIBS) -d html $(VFILES)
-
-all.ps: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -ps $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.ps: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -ps -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all.pdf: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -pdf $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-all-gal.pdf: $(VFILES)
-	$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`
-
-validate: $(VOFILES)
-	$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))
-
-beautify: $(VFILES:=.beautified)
-	for file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done
-	@echo 'Do not do "make clean" until you are sure that everything went well!'
-	@echo 'If there were a problem, execute "for file in $$(find . -name \*.v.old -print); do mv $${file} $${file%.old}; done" in your shell/'
-
-.PHONY: all opt byte archclean clean install userinstall depend html validate
-
-###################
-#                 #
-# Custom targets. #
-#                 #
-###################
-
-$(CMXS): $(CMXA)
-	$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^
-
-$(CMXA): versions/native/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtBtype.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx trace/smtMaps.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx ../3rdparty/alt-ergo/smtlib2_util.cmx ../3rdparty/alt-ergo/smtlib2_ast.cmx ../3rdparty/alt-ergo/smtlib2_parse.cmx ../3rdparty/alt-ergo/smtlib2_lex.cmx smtlib2/sExpr.cmx smtlib2/sExprParser.cmx smtlib2/sExprLexer.cmx smtlib2/smtlib2_solver.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx lfsc/shashcons.cmx lfsc/hstring.cmx lfsc/type.cmx lfsc/ast.cmx lfsc/builtin.cmx lfsc/tosmtcoq.cmx lfsc/converter.cmx lfsc/lfscParser.cmx lfsc/lfscLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx lfsc/lfsc.cmx smtcoq_plugin.cmx
-	$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
-
-ml: verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
-
-
-%.ml %.mli: %.mly
-	$(CAMLYACC) $<
-
-%.ml: %.mll
-	$(CAMLLEX) $<
-
-vtest: 
-	cd ../unit-tests; make veritv
-
-ztest: 
-	cd ../unit-tests; make zchaffv
-
-test: 
-	cd ../unit-tests; make vernac
-
-####################
-#                  #
-# Special targets. #
-#                  #
-####################
-
-byte:
-	$(MAKE) all "OPT:=-byte"
-
-opt:
-	$(MAKE) all "OPT:=-opt"
-
-userinstall:
-	+$(MAKE) USERINSTALL=true install
-
-install-natdynlink:
-	for i in $(CMXS); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-	for i in $(CMXA); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-	for i in $(VCMXS); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-
-install:$(if ifeq '$(HASNATDYNLINK)' 'true',install-natdynlink)
-	for i in $(VOFILES) $(OBJFILES) $(OBJFILES:.o=.cm*); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-	for i in $(CMXFILES); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-	for i in $(CMIFILES); do \
-	 install -d `dirname $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i`; \
-	 install -m 0644 $$i $(DSTROOT)$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-
-install-doc:
-	install -d $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/html
-	for i in html/*; do \
-	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/$$i;\
-	done
-	install -d $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/mlihtml
-	for i in mlihtml/*; do \
-	 install -m 0644 $$i $(DSTROOT)$(COQDOCINSTALL)/SMTCoq/$$i;\
-	done
-
-clean:
-	rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)
-	rm -f $(ALLCMOFILES:.cmo=.cmx) $(CMXAFILES) $(CMXSFILES) $(ALLCMOFILES:.cmo=.o) $(CMXAFILES:.cmxa=.a)
-	rm -f $(addsuffix .d,$(MLFILES) $(MLIFILES) $(ML4FILES) $(MLLIBFILES) $(MLPACKFILES))
-	rm -f $(OBJFILES) $(OBJFILES:.o=.native)
-	rm -f $(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo)
-	rm -f $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
-	rm -f $(VOFILES) $(VIFILES) $(GFILES) $(VFILES:.v=.v.d) $(VFILES:=.beautified) $(VFILES:=.old)
-	rm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) all-mli.tex
-	- rm -rf html mlihtml
-	- rm -rf $(CMXS)
-	- rm -rf $(CMXA)
-	- rm -rf ml
-	- rm -rf vtest
-	- rm -rf ztest
-	- rm -rf test
-	- rm -f NSMTCoq* cnf/NSMTCoq* euf/NSMTCoq* lia/NSMTCoq* spl/NSMTCoq* ../unit-tests/NSMTCoq* ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml ../3rdparty/alt-ergo/smtlib2_parse.mli ../3rdparty/alt-ergo/smtlib2_parse.ml ../3rdparty/alt-ergo/smtlib2_lex.ml smtlib2/sExprParser.mli smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscLexer.ml lfsc/lfscParser.ml lfsc/lfscParser.mli trace/smtcoq.a
-
-archclean:
-	rm -f *.cmx *.o
-
-printenv:
-	@$(COQBIN)coqtop -config
-	@echo CAMLC =	$(CAMLC)
-	@echo CAMLOPTC =	$(CAMLOPTC)
-	@echo PP =	$(PP)
-	@echo COQFLAGS =	$(COQFLAGS)
-	@echo COQLIBINSTALL =	$(COQLIBINSTALL)
-	@echo COQDOCINSTALL =	$(COQDOCINSTALL)
-
-
-###################
-#                 #
-# Implicit rules. #
-#                 #
-###################
-
-%.cmi: %.mli
-	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
-
-%.mli.d: %.mli
-	$(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.cmo: %.ml4
-	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
-
-%.cmx: %.ml4
-	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
-
-%.ml4.d: %.ml4
-	$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.cmo: %.ml
-	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
-
-%.cmx: %.ml
-	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<
-
-%.ml.d: %.ml
-	$(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.cmxs: %.cmx
-	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<
-
-%.vo %.glob: %.v
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $*
-
-%.vi: %.v
-	$(COQC) -i $(COQDEBUG) $(COQFLAGS) $*
-
-%.g: %.v
-	$(GALLINA) $<
-
-%.tex: %.v
-	$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@
-
-%.html: %.v %.glob
-	$(COQDOC) $(COQDOCFLAGS) -html $< -o $@
-
-%.g.tex: %.v
-	$(COQDOC) $(COQDOCFLAGS) -latex -g $< -o $@
-
-%.g.html: %.v %.glob
-	$(COQDOC)$(COQDOCFLAGS)  -html -g $< -o $@
-
-%.v.d: %.v
-	$(COQDEP) -slash $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
-
-%.v.beautified:
-	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*
-
-# WARNING
-#
-# This Makefile has been automagically generated
-# Edit at your own risks !
-#
-# END OF WARNING
-
diff --git a/src/versions/native/Structures_native.v b/src/versions/native/Structures_native.v
deleted file mode 100644
index 47ae21f..0000000
--- a/src/versions/native/Structures_native.v
+++ /dev/null
@@ -1,59 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2021                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-Require Import PArray.
-
-
-Section Trace.
-
-  (* We use [array array step] to allow bigger trace *)
-  Definition trace (step:Type) := array (array step).
-
-  Definition trace_to_list {step:Type} (t:trace step) : list step :=
-    PArray.fold_left (fun res a => List.app res (PArray.to_list a)) nil t.
-
-  Definition trace_length {step:Type} (t:trace step) : int :=
-    PArray.fold_left (fun l a => (l + (length a))%int63) 0%int63 t.
-
-  Definition trace_get {step:Type} (t:trace step) (i:int) : step :=
-    snd (PArray.fold_left (fun (jres:(option int) * step) a =>
-                        let (j,res) := jres in
-                        match j with
-                        | Some j' =>
-                          let l := length a in
-                          if (j' < l)%int63 then
-                            (None, get a j')
-                          else
-                            ((Some ((j' - l)%int63)),res)
-                        | None => (None,res)
-                        end
-                     ) (Some i, (get (get t 0) 0)) t).
-
-  Definition trace_fold {state step:Type} (transition: state -> step -> state) (s0:state) (t:trace step) :=
-    PArray.fold_left (PArray.fold_left transition) s0 t.
-
-  Lemma trace_fold_ind (state step : Type) (P : state -> Prop) (transition : state -> step -> state) (t : trace step)
-      (IH: forall (s0 : state) (i : int), (i < trace_length t)%int63 = true -> P s0 -> P (transition s0 (trace_get t i))) :
-      forall s0 : state, P s0 -> P (trace_fold transition s0 t).
-  Proof.
-    apply PArray.fold_left_ind.
-    intros a i Hi Ha.
-    apply PArray.fold_left_ind;trivial.
-    intros a0 i0 Hi0 Ha0.       (* IH applied to a0 and (sum of the lengths of the first i arrays + i0) *)
-  Admitted.
-
-End Trace.
-
-
-Definition nat_eqb := beq_nat.
-Definition nat_eqb_eq := beq_nat_true_iff.
-Definition nat_eqb_refl := NPeano.Nat.eqb_refl.
diff --git a/src/versions/native/Tactics_native.v b/src/versions/native/Tactics_native.v
deleted file mode 100644
index 45d3603..0000000
--- a/src/versions/native/Tactics_native.v
+++ /dev/null
@@ -1,55 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2021                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-Require Import Psatz.
-
-Declare ML Module "smtcoq_plugin".
-
-
-
-Tactic Notation "verit_bool" constr_list(h) :=
-  fail "Tactics are not supported with native-coq".
-
-Tactic Notation "verit_bool_no_check" constr_list(h) :=
-  fail "Tactics are not supported with native-coq".
-
-
-(** Tactics in Prop **)
-
-Ltac zchaff          :=
-  fail "Tactics are not supported with native-coq".
-Ltac zchaff_no_check :=
-  fail "Tactics are not supported with native-coq".
-
-Tactic Notation "verit" constr_list(h) :=
-  fail "Tactics are not supported with native-coq".
-Tactic Notation "verit_no_check" constr_list(h) :=
-  fail "Tactics are not supported with native-coq".
-
-Ltac cvc4            :=
-  fail "Tactics are not supported with native-coq".
-Ltac cvc4_no_check   :=
-  fail "Tactics are not supported with native-coq".
-
-
-Tactic Notation "smt" constr_list(h) :=
-  fail "Tactics are not supported with native-coq".
-Tactic Notation "smt_no_check" constr_list(h) :=
-  fail "Tactics are not supported with native-coq".
-
-
-
-(* 
-   Local Variables:
-   coq-load-path: ((rec "../.." "SMTCoq"))
-   End: 
-*)
diff --git a/src/versions/native/smtcoq_plugin_native.ml4 b/src/versions/native/smtcoq_plugin_native.ml4
deleted file mode 100644
index ebf8511..0000000
--- a/src/versions/native/smtcoq_plugin_native.ml4
+++ /dev/null
@@ -1,99 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2021                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-VERNAC COMMAND EXTEND Vernac_zchaff
-| [ "Parse_certif_zchaff" 
-    ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] ->
-  [
-    Zchaff.parse_certif dimacs trace fdimacs fproof
-  ]
-| [ "Zchaff_Checker" string(fdimacs) string(fproof) ] ->
-  [
-    Zchaff.checker fdimacs fproof
-  ]
-| [ "Zchaff_Theorem" ident(name) string(fdimacs) string(fproof) ] ->
-  [
-    Zchaff.theorem name fdimacs fproof
-  ]
-END
-
-VERNAC COMMAND EXTEND Vernac_zchaff_abs
-| [ "Zchaff_Theorem_Abs" ident(name) string(fdimacs) string(fproof) ] ->
-  [
-    Zchaff.theorem_abs name fdimacs fproof
-  ]
-END
-
-VERNAC COMMAND EXTEND Vernac_verit
-| [ "Parse_certif_verit"
-    ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] ->
-  [
-    Verit.parse_certif t_i t_func t_atom t_form root used_roots trace fsmt fproof
-  ]
-| [ "Verit_Checker" string(fsmt) string(fproof) ] ->
-  [
-    Verit.checker fsmt fproof
-  ]
-| [ "Verit_Checker_Debug" string(fsmt) string(fproof) ] ->
-  [
-    Verit.checker_debug fsmt fproof
-  ]
-| [ "Verit_Theorem" ident(name) string(fsmt) string(fproof) ] ->
-  [
-    Verit.theorem name fsmt fproof
-  ]
-END
-
-VERNAC COMMAND EXTEND Vernac_lfsc
-| [ "Parse_certif_lfsc"
-    ident(t_i) ident(t_func) ident(t_atom) ident(t_form) ident(root) ident(used_roots) ident(trace) string(fsmt) string(fproof) ] ->
-  [
-    Lfsc.parse_certif t_i t_func t_atom t_form root used_roots trace fsmt fproof
-  ]
-| [ "Lfsc_Checker" string(fsmt) string(fproof) ] ->
-  [
-    Lfsc.checker fsmt fproof
-  ]
-| [ "Lfsc_Checker_Debug" string(fsmt) string(fproof) ] ->
-  [
-    Lfsc.checker_debug fsmt fproof
-  ]
-| [ "Lfsc_Theorem" ident(name) string(fsmt) string(fproof) ] ->
-  [
-    Lfsc.theorem name fsmt fproof
-  ]
-END
-
-TACTIC EXTEND Tactic_zchaff
-| [ "zchaff_bool" ] -> [ Zchaff.tactic () ]
-| [ "zchaff_bool_no_check" ] -> [ Zchaff.tactic_no_check () ]
-END
-
-let lemmas_list = ref []
-
-VERNAC COMMAND EXTEND Add_lemma
-| [ "Add_lemmas" constr_list(lems) ] -> [ lemmas_list := lems @ !lemmas_list ]
-| [ "Clear_lemmas" ] -> [ lemmas_list := [] ]
-END
-
-
-let error () = Structures.error "Tactics are not supported with native-coq"
-
-TACTIC EXTEND Tactic_verit
-| [ "verit_bool_base" constr_list(lpl) ] -> [ error () ]
-| [ "verit_bool_no_check_base" constr_list(lpl) ] -> [ error () ]
-END
-
-TACTIC EXTEND Tactic_cvc4
-| [ "cvc4_bool" ] -> [ error () ]
-| [ "cvc4_bool_no_check" ] -> [ error () ]
-END
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
deleted file mode 100644
index 435a1a1..0000000
--- a/src/versions/native/structures.ml
+++ /dev/null
@@ -1,186 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2021                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-open Entries
-open Coqlib
-
-
-(* Constr generation and manipulation *)
-type id = Names.identifier
-let mkId = Names.id_of_string
-
-
-type name = Names.name
-let name_of_id i = Names.Name i
-let mkName s =
-  let id = mkId s in
-  name_of_id id
-let string_of_name = function
-    Names.Name id -> Names.string_of_id id
-  | _ -> failwith "unnamed rel"
-
-
-type constr = Term.constr
-type types = Term.types
-let eq_constr = Term.eq_constr
-let hash_constr = Term.hash_constr
-let mkProp = Term.mkProp
-let mkConst = Term.mkConst
-let mkVar = Term.mkVar
-let mkRel = Term.mkRel
-let isRel = Term.isRel
-let destRel = Term.destRel
-let lift = Term.lift
-let mkApp = Term.mkApp
-let decompose_app = Term.decompose_app
-let mkLambda = Term.mkLambda
-let mkProd = Term.mkProd
-let mkLetIn = Term.mkLetIn
-
-let pr_constr_env = Printer.pr_constr_env
-let pr_constr = Printer.pr_constr
-
-
-let dummy_loc = Pp.dummy_loc
-
-let mkUConst c =
-  { const_entry_body = c;
-    const_entry_type = None;
-    const_entry_secctx = None;
-    const_entry_opaque = false;
-    const_entry_inline_code = false}
-
-let mkTConst c _ ty =
-  { const_entry_body = c;
-    const_entry_type = Some ty;
-    const_entry_secctx = None;
-    const_entry_opaque = false;
-    const_entry_inline_code = false}
-
-(* TODO : Set -> Type *)
-let declare_new_type t =
-  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) Term.mkSet [] false None (dummy_loc, t);
-  Term.mkVar t
-
-let declare_new_variable v constr_t =
-  Command.declare_assumption false (Decl_kinds.Local,Decl_kinds.Definitional) constr_t [] false None (dummy_loc, v);
-  Term.mkVar v
-
-let declare_constant n c =
-  Declare.declare_constant n (DefinitionEntry c, Decl_kinds.IsDefinition Decl_kinds.Definition)
-
-
-type cast_kind = Term.cast_kind
-let vmcast = Term.VMcast
-let mkCast = Term.mkCast
-
-
-(* EConstr *)
-type econstr = Term.constr
-let econstr_of_constr e = e
-
-
-(* Modules *)
-let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
-
-
-(* Int63 *)
-let int63_modules = [["Coq";"Numbers";"Cyclic";"Int63";"Int63Native"]]
-
-let mkInt : int -> Term.constr =
-  fun i -> Term.mkInt (Uint63.of_int i)
-
-let cint = gen_constant int63_modules "int"
-
-
-(* PArray *)
-let parray_modules = [["Coq";"Array";"PArray"]]
-
-let max_array_size : int =
-  Parray.trunc_size (Uint63.of_int 4194303)
-let mkArray : Term.types * Term.constr array -> Term.constr =
-  Term.mkArray
-
-
-(* Traces *)
-(* WARNING: side effect on r! *)
-let mkTrace step_to_coq next carray _ _ _ _ size step def_step r =
-  let max = max_array_size - 1 in
-  let q,r1 = size / max, size mod max in
-  let trace =
-    let len = if r1 = 0 then q + 1 else q + 2 in
-    Array.make len (mkArray (step, [|def_step|])) in
-  for j = 0 to q - 1 do
-    let tracej = Array.make max_array_size def_step in
-    for i = 0 to max - 1 do
-      r := next !r;
-      tracej.(i) <- step_to_coq !r;
-    done;
-    trace.(j) <- mkArray (step, tracej)
-  done;
-  if r1 <> 0 then (
-    let traceq = Array.make (r1 + 1) def_step in
-    for i = 0 to r1-1 do
-      r := next !r;
-    traceq.(i) <- step_to_coq !r;
-    done;
-    trace.(q) <- mkArray (step, traceq)
-  );
-  mkArray (Term.mkApp (Lazy.force carray, [|step|]), trace)
-
-
-(* Micromega *)
-module Micromega_plugin_Micromega = Micromega
-module Micromega_plugin_Certificate = Certificate
-
-let micromega_coq_proofTerm =
-  Coq_micromega.M.coq_proofTerm
-
-let micromega_dump_proof_term p =
-  Coq_micromega.dump_proof_term p
-
-
-(* Tactics *)
-type tactic = Proof_type.tactic
-let tclTHEN = Tacticals.tclTHEN
-let tclTHENLAST = Tacticals.tclTHENLAST
-let assert_before = Tactics.assert_tac
-let vm_cast_no_check = Tactics.vm_cast_no_check
-let mk_tactic tac gl =
-  let env = Tacmach.pf_env gl in
-  let sigma = Tacmach.project gl in
-  let t = Tacmach.pf_concl gl in
-  tac env sigma t gl
-let set_evars_tac _ = Tacticals.tclIDTAC
-
-
-(* Other differences between the two versions of Coq *)
-type constr_expr = Topconstr.constr_expr
-let error = Errors.error
-let warning _ s = Pp.warning s
-let extern_constr = Constrextern.extern_constr true Environ.empty_env
-let destruct_rel_decl (n, _, t) = n, t
-let interp_constr env sigma = Constrintern.interp_constr sigma env
-let ppconstr_lsimpleconstr = Ppconstr.lsimple
-let constrextern_extern_constr =
-  let env = Global.env () in
-  Constrextern.extern_constr false env
-
-let get_rel_dec_name = fun _ -> Names.Anonymous
-
-(* Eta-expanded to get rid of optional arguments *)
-let retyping_get_type_of env = Retyping.get_type_of env
-
-let vm_conv = Reduction.vm_conv
-let cbv_vm = Vnorm.cbv_vm
-
-
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
deleted file mode 100644
index f2775a6..0000000
--- a/src/versions/native/structures.mli
+++ /dev/null
@@ -1,117 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2021                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-(* Constr generation and manipulation *)
-type id = Names.variable
-val mkId : string -> id
-
-type name
-val name_of_id : id -> name
-val mkName : string -> name
-val string_of_name : name -> string
-
-type constr = Term.constr
-type types = constr
-val eq_constr : constr -> constr -> bool
-val hash_constr : constr -> int
-val mkProp : types
-val mkConst : Names.constant -> constr
-val mkVar : id -> constr
-val mkRel : int -> constr
-val isRel : constr -> bool
-val destRel : constr -> int
-val lift : int -> constr -> constr
-val mkApp : constr * constr array -> constr
-val decompose_app : constr -> constr * constr list
-val mkLambda : name * types * constr -> constr
-val mkProd : name * types * types -> types
-val mkLetIn : name * constr * types * constr -> constr
-
-val pr_constr_env : Environ.env -> constr -> Pp.std_ppcmds
-val pr_constr : constr -> Pp.std_ppcmds
-
-val mkUConst : constr -> Entries.definition_entry
-val mkTConst : constr -> 'a -> types -> Entries.definition_entry
-val declare_new_type : id -> types
-val declare_new_variable : id -> types -> constr
-val declare_constant : id -> Entries.definition_entry -> Names.constant
-
-type cast_kind
-val vmcast : cast_kind
-val mkCast : constr * cast_kind * constr -> constr
-
-
-(* EConstr *)
-type econstr = constr
-val econstr_of_constr : constr -> econstr
-
-
-(* Modules *)
-val gen_constant : string list list -> string -> constr lazy_t
-
-
-(* Int63 *)
-val int63_modules : 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 *)
-val mkTrace :
-  ('a -> constr) ->
-  ('a -> 'a) ->
-  constr Lazy.t ->
-  'b ->
-  'c -> 'd -> 'e -> int -> types -> constr -> 'a ref -> constr
-
-
-(* Micromega *)
-module Micromega_plugin_Micromega = Micromega
-module Micromega_plugin_Certificate = Certificate
-
-val micromega_coq_proofTerm : constr lazy_t
-val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr
-
-
-(* Tactics *)
-type tactic = Proof_type.tactic
-val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
-val tclTHENLAST : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic
-val assert_before : name -> types -> Proof_type.tactic
-val vm_cast_no_check : constr -> Proof_type.tactic
-val mk_tactic :
-  (Environ.env ->
-   Evd.evar_map -> types -> Proof_type.goal Tacmach.sigma -> 'a) ->
-  Proof_type.goal Tacmach.sigma -> 'a
-val set_evars_tac : 'a -> Proof_type.tactic
-
-
-(* Other differences between the two versions of Coq *)
-type constr_expr = Topconstr.constr_expr
-val error : string -> 'a
-val warning : string -> string -> unit
-val extern_constr : constr -> Topconstr.constr_expr
-val destruct_rel_decl : Term.rel_declaration -> name * types
-val interp_constr : Environ.env -> Evd.evar_map -> Topconstr.constr_expr -> constr
-val ppconstr_lsimpleconstr : Ppconstr.precedence
-val constrextern_extern_constr : constr -> Topconstr.constr_expr
-val get_rel_dec_name : 'a -> name
-val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr
-
-val vm_conv : Reduction.conv_pb -> types Reduction.conversion_function
-val cbv_vm : Environ.env -> constr -> types -> constr
diff --git a/src/versions/standard/Structures_standard.v b/src/versions/standard/Structures_standard.v
deleted file mode 100644
index 1a0abf5..0000000
--- a/src/versions/standard/Structures_standard.v
+++ /dev/null
@@ -1,64 +0,0 @@
-(**************************************************************************)
-(*                                                                        *)
-(*     SMTCoq                                                             *)
-(*     Copyright (C) 2011 - 2021                                          *)
-(*                                                                        *)
-(*     See file "AUTHORS" for the list of authors                         *)
-(*                                                                        *)
-(*   This file is distributed under the terms of the CeCILL-C licence     *)
-(*                                                                        *)
-(**************************************************************************)
-
-
-Require Import Int63.
-
-Require Import List.
-
-
-Section Trace.
-
-  Definition trace (step:Type) := ((list step) * step)%type.
-
-  Definition trace_to_list {step:Type} (t:trace step) : list step :=
-    let (t, _) := t in t.
-
-  Definition trace_length {step:Type} (t:trace step) : int :=
-    let (t,_) := t in
-    List.fold_left (fun i _ => (i+1)%int) t 0%int.
-
-  Fixpoint trace_get_aux {step:Type} (t:list step) (def:step) (i:int) : step :=
-    match t with
-    | nil => def
-    | s::ss =>
-      if (i == 0)%int then
-        s
-      else
-        trace_get_aux ss def (i-1)
-    end.
-  Definition trace_get {step:Type} (t:trace step) : int -> step :=
-    let (t,def) := t in trace_get_aux t def.
-
-  Definition trace_fold {state step:Type} (transition: state -> step -> state) (s0:state) (t:trace step) :=
-    let (t,_) := t in
-    List.fold_left transition t s0.
-
-  Lemma trace_fold_ind (state step : Type) (P : state -> Prop) (transition : state -> step -> state) (t : trace step)
-      (IH: forall (s0 : state) (i : int), (i < trace_length t)%int = true -> P s0 -> P (transition s0 (trace_get t i))) :
-      forall s0 : state, P s0 -> P (trace_fold transition s0 t).
-  Admitted.
-
-End Trace.
-
-
-Require Import PeanoNat.
-
-Definition nat_eqb := Nat.eqb.
-Definition nat_eqb_eq := Nat.eqb_eq.
-Definition nat_eqb_refl := Nat.eqb_refl.
-
-
-(*
-   Local Variables:
-   coq-load-path: ((rec "../.." "SMTCoq"))
-   End:
-*)
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index c6bdc64..1f5110b 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) (Structures.mkArray (cint, Array.make 1 (mkInt 0))) in
+  let roots = Array.make (last.id + 2) (CoqInterface.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) <- Structures.mkArray (cint, croot);
+    roots.(!r.id) <- CoqInterface.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) <- Structures.mkArray (cint, croot);
+  roots.(!r.id) <- CoqInterface.mkArray (cint, croot);
 
-  Structures.mkArray (mklApp carray [|cint|], roots)
+  CoqInterface.mkArray (mklApp carray [|cint|], roots)
 
 let interp_roots first last =
   let tbl = Hashtbl.create 17 in
@@ -164,7 +164,7 @@ let interp_roots first last =
     let h = if Form.is_pos l then ph else ph lxor 1 in
     try Hashtbl.find tbl h
     with Not_found ->
-      let p = Structures.mkApp (Structures.mkRel 1, [|mkInt (x+1)|]) in
+      let p = CoqInterface.mkApp (CoqInterface.mkRel 1, [|mkInt (x+1)|]) in
       let np = mklApp cnegb [|p|] in
       Hashtbl.add tbl ph p;
       Hashtbl.add tbl (ph lxor 1) np;
@@ -194,15 +194,15 @@ let parse_certif dimacs trace fdimacs ftrace =
   SmtTrace.clear ();
   let _,first,last,reloc = import_cnf fdimacs in
   let d = make_roots first last in
-  let ce1 = Structures.mkUConst d in
-  let _ = Structures.declare_constant dimacs ce1 in
+  let ce1 = CoqInterface.mkUConst d in
+  let _ = CoqInterface.declare_constant dimacs ce1 in
 
   let max_id, confl = import_cnf_trace reloc ftrace first last in
   let (tres,_,_) = SmtTrace.to_coq (fun _ -> assert false) (fun _ -> assert false) certif_ops confl None in
   let certif =
    mklApp cCertif [|mkInt (max_id + 1); tres;mkInt (get_pos confl)|] in
-  let ce2 = Structures.mkUConst certif in
-  let _ = Structures.declare_constant trace ce2 in
+  let ce2 = CoqInterface.mkUConst certif in
+  let _ = CoqInterface.declare_constant trace ce2 in
   ()
 
 let cdimacs = gen_constant sat_checker_modules "dimacs"
@@ -222,36 +222,36 @@ let theorems interp name fdimacs ftrace =
    mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
 
   let theorem_concl = mklApp cnot [|mklApp cis_true [|interp d first last|] |] in
-  let vtype = Structures.mkArrow (Lazy.force cint) (Lazy.force cbool) in
+  let vtype = CoqInterface.mkArrow (Lazy.force cint) (Lazy.force cbool) in
   let theorem_type =
-    Structures.mkProd (Structures.mkName "v", vtype, theorem_concl) in
+    CoqInterface.mkProd (CoqInterface.mkName "v", vtype, theorem_concl) in
   let theorem_proof_cast =
-    Structures.mkCast (
-        Structures.mkLetIn (Structures.mkName "d", d, Lazy.force cdimacs,
-        Structures.mkLetIn (Structures.mkName "c", certif, Lazy.force ccertif,
-        Structures.mkLambda (Structures.mkName "v", vtype,
+    CoqInterface.mkCast (
+        CoqInterface.mkLetIn (CoqInterface.mkName "d", d, Lazy.force cdimacs,
+        CoqInterface.mkLetIn (CoqInterface.mkName "c", certif, Lazy.force ccertif,
+        CoqInterface.mkLambda (CoqInterface.mkName "v", vtype,
         mklApp ctheorem_checker
-               [| Structures.mkRel 3(*d*); Structures.mkRel 2(*c*);
+               [| CoqInterface.mkRel 3(*d*); CoqInterface.mkRel 2(*c*);
 		  vm_cast_true_no_check
-		    (mklApp cchecker [|Structures.mkRel 3(*d*); Structures.mkRel 2(*c*)|]);
-                  Structures.mkRel 1(*v*)|]))),
-      Structures.vmcast,
+		    (mklApp cchecker [|CoqInterface.mkRel 3(*d*); CoqInterface.mkRel 2(*c*)|]);
+                  CoqInterface.mkRel 1(*v*)|]))),
+      CoqInterface.vmcast,
       theorem_type)
   in
   let theorem_proof_nocast =
-    Structures.mkLetIn (Structures.mkName "d", d, Lazy.force cdimacs,
-    Structures.mkLetIn (Structures.mkName "c", certif, Lazy.force ccertif,
-    Structures.mkLambda (Structures.mkName "v", vtype,
+    CoqInterface.mkLetIn (CoqInterface.mkName "d", d, Lazy.force cdimacs,
+    CoqInterface.mkLetIn (CoqInterface.mkName "c", certif, Lazy.force ccertif,
+    CoqInterface.mkLambda (CoqInterface.mkName "v", vtype,
     mklApp ctheorem_checker
-           [| Structures.mkRel 3(*d*); Structures.mkRel 2(*c*)|])))
+           [| CoqInterface.mkRel 3(*d*); CoqInterface.mkRel 2(*c*)|])))
   in
-  let ce = Structures.mkTConst theorem_proof_cast theorem_proof_nocast theorem_type in
-  let _ = Structures.declare_constant name ce in
+  let ce = CoqInterface.mkTConst theorem_proof_cast theorem_proof_nocast theorem_type in
+  let _ = CoqInterface.declare_constant name ce in
   ()
 
 let theorem = theorems (fun _ -> interp_roots)
 let theorem_abs =
-  theorems (fun d _ _ -> mklApp cvalid_sat_checker [|mklApp cinterp_var_sat_checker [|Structures.mkRel 1(*v*)|]; d|])
+  theorems (fun d _ _ -> mklApp cvalid_sat_checker [|mklApp cinterp_var_sat_checker [|CoqInterface.mkRel 1(*v*)|]; d|])
 
 
 let checker fdimacs ftrace =
@@ -267,9 +267,9 @@ let checker fdimacs ftrace =
 
   let tm = mklApp cchecker [|d; certif|] 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")
 
 
@@ -358,22 +358,22 @@ let cchecker_eq_correct =
 let cchecker_eq = gen_constant cnf_checker_modules "checker_eq"
 
 let build_body reify_atom reify_form l b (max_id, confl) vm_cast =
-  let ntvar = Structures.mkName "t_var" in
-  let ntform = Structures.mkName "t_form" in
-  let nc = Structures.mkName "c" in
+  let ntvar = CoqInterface.mkName "t_var" in
+  let ntform = CoqInterface.mkName "t_form" in
+  let nc = CoqInterface.mkName "c" in
   let tvar = Atom.interp_tbl reify_atom in
   let _, tform = Form.interp_tbl reify_form in
   let (tres,_,_) =
     SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in
   let certif =
     mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
-  let vtvar = Structures.mkRel 3 in
-  let vtform = Structures.mkRel 2 in
-  let vc = Structures.mkRel 1 in
+  let vtvar = CoqInterface.mkRel 3 in
+  let vtform = CoqInterface.mkRel 2 in
+  let vc = CoqInterface.mkRel 1 in
   let add_lets t =
-    Structures.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
-    Structures.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
-    Structures.mkLetIn (nc, certif, Lazy.force ccertif,
+    CoqInterface.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
+    CoqInterface.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
+    CoqInterface.mkLetIn (nc, certif, Lazy.force ccertif,
     t)))
   in
   let cbc =
@@ -391,22 +391,22 @@ let build_body reify_atom reify_form l b (max_id, confl) vm_cast =
 
 
 let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) vm_cast =
-  let ntvar = Structures.mkName "t_var" in
-  let ntform = Structures.mkName "t_form" in
-  let nc = Structures.mkName "c" in
+  let ntvar = CoqInterface.mkName "t_var" in
+  let ntform = CoqInterface.mkName "t_form" in
+  let nc = CoqInterface.mkName "c" in
   let tvar = Atom.interp_tbl reify_atom in
   let _, tform = Form.interp_tbl reify_form in
   let (tres,_,_) =
     SmtTrace.to_coq Form.to_coq (fun _ -> assert false) certif_ops confl None in
   let certif =
     mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
-  let vtvar = Structures.mkRel 3 in
-  let vtform = Structures.mkRel 2 in
-  let vc = Structures.mkRel 1 in
+  let vtvar = CoqInterface.mkRel 3 in
+  let vtform = CoqInterface.mkRel 2 in
+  let vc = CoqInterface.mkRel 1 in
   let add_lets t =
-    Structures.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
-    Structures.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
-    Structures.mkLetIn (nc, certif, Lazy.force ccertif,
+    CoqInterface.mkLetIn (ntvar, tvar, mklApp carray [|Lazy.force cbool|],
+    CoqInterface.mkLetIn (ntform, tform, mklApp carray [|Lazy.force cform|],
+    CoqInterface.mkLetIn (nc, certif, Lazy.force ccertif,
     t)))
   in
   let ceqc = add_lets (mklApp cchecker_eq [|vtform;l1;l2;l;vc|])
@@ -421,10 +421,10 @@ let build_body_eq reify_atom reify_form l1 l2 l (max_id, confl) vm_cast =
   (proof_cast, proof_nocast)
 
 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 ("Zchaff.get_arguments :can only deal with equality over bool")
 
 
@@ -499,7 +499,7 @@ let make_proof pform_tbl atom_tbl env reify_form l =
   let (reloc, resfilename, logfilename, last) =
     call_zchaff (Form.nvars reify_form) root in
   (try check_unsat resfilename with
-    | Sat model -> Structures.error (List.fold_left (fun acc i ->
+    | Sat model -> CoqInterface.error (List.fold_left (fun acc i ->
       let index = if i > 0 then i-1 else -i-1 in
       let ispos = i > 0 in
       try (
@@ -508,7 +508,7 @@ let make_proof pform_tbl atom_tbl env reify_form l =
           | Fatom a ->
             let t = atom_tbl.(a) in
             let value = if ispos then " = true" else " = false" in
-            acc^"  "^(Pp.string_of_ppcmds (Structures.pr_constr_env env t))^value
+            acc^"  "^(Pp.string_of_ppcmds (CoqInterface.pr_constr_env env t))^value
           | Fapp _ -> acc
           (* Nothing to do with ZChaff *)
           | FbbT _ -> assert false
@@ -528,9 +528,9 @@ let core_tactic vm_cast env sigma concl =
   let reify_atom = Atom.create () in
   let reify_form = Form.create () in
   let (body_cast, body_nocast) =
-    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.get reify_atom) reify_form a in
-      let l' = if (Structures.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
+      let l' = if (CoqInterface.eq_constr b (Lazy.force ctrue)) then Form.neg l else l in
       let atom_tbl = Atom.atom_tbl reify_atom in
       let pform_tbl = Form.pform_tbl reify_form in
       let max_id_confl = make_proof pform_tbl atom_tbl (Environ.push_rel_context forall_let env) reify_form l' in
@@ -551,10 +551,10 @@ let core_tactic vm_cast env sigma concl =
   let res_cast = compose_lam_assum forall_let body_cast in
   let res_nocast = compose_lam_assum forall_let body_nocast in
 
-  (Structures.tclTHEN
-     (Structures.set_evars_tac res_nocast)
-     (Structures.vm_cast_no_check res_cast))
+  (CoqInterface.tclTHEN
+     (CoqInterface.set_evars_tac res_nocast)
+     (CoqInterface.vm_cast_no_check res_cast))
 
 
-let tactic () = Structures.tclTHEN Tactics.intros (Structures.mk_tactic (core_tactic vm_cast_true))
-let tactic_no_check () = Structures.tclTHEN Tactics.intros (Structures.mk_tactic (core_tactic (fun _ -> vm_cast_true_no_check)))
+let tactic () = CoqInterface.tclTHEN Tactics.intros (CoqInterface.mk_tactic (core_tactic vm_cast_true))
+let tactic_no_check () = CoqInterface.tclTHEN Tactics.intros (CoqInterface.mk_tactic (core_tactic (fun _ -> vm_cast_true_no_check)))
diff --git a/src/zchaff/zchaff.mli b/src/zchaff/zchaff.mli
index 3f458d3..1e472fc 100644
--- a/src/zchaff/zchaff.mli
+++ b/src/zchaff/zchaff.mli
@@ -11,9 +11,9 @@
 
 
 val pp_trace : Format.formatter -> SatAtom.Form.t SmtCertif.clause -> unit
-val parse_certif : Structures.id -> Structures.id -> string -> string -> unit
+val parse_certif : CoqInterface.id -> CoqInterface.id -> string -> string -> unit
 val checker : string -> string -> unit
-val theorem : Structures.id -> string -> string -> unit
-val theorem_abs : Structures.id -> string -> string -> unit
-val tactic : unit -> Structures.tactic
-val tactic_no_check : unit -> Structures.tactic
+val theorem : CoqInterface.id -> string -> string -> unit
+val theorem_abs : CoqInterface.id -> string -> string -> unit
+val tactic : unit -> CoqInterface.tactic
+val tactic_no_check : unit -> CoqInterface.tactic