Compiles with Coq-8.6

14 files changed, 296 insertions, 151 deletions

diff --git a/src/configure.sh b/src/configure.sh
index 6e044a8..a9d124b 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -8,7 +8,8 @@ if [ $@ -a $@ = -native ]; then
     cp versions/native/Structures_native.v versions/native/Structures.v
 else
     cp versions/standard/Makefile Makefile
-    cp versions/standard/smtcoq_plugin_standard.ml4 smtcoq_plugin.ml4
+    cp versions/standard/g_smtcoq_standard.ml4 g_smtcoq.ml4
+    cp versions/standard/smtcoq_plugin_standard.mlpack smtcoq_plugin.mlpack
     cp versions/standard/Int63/Int63_standard.v versions/standard/Int63/Int63.v
     cp versions/standard/Int63/Int63Native_standard.v versions/standard/Int63/Int63Native.v
     cp versions/standard/Int63/Int63Op_standard.v versions/standard/Int63/Int63Op.v
diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index de291da..07064bb 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -21,9 +21,8 @@ open Declare
 open Decl_kinds
 open Entries
 open Util
-open Micromega
-open Coq_micromega
-open Errors
+(* open Micromega *)
+(* open Coq_micromega *)
 
 open SmtMisc
 open SmtForm
@@ -33,19 +32,19 @@ open SmtAtom
 
 let rec pos_of_int i =
   if i <= 1
-  then XH
+  then Micromega_plugin.Micromega.XH
   else
     if i land 1 = 0
-    then XO(pos_of_int (i lsr 1))
-    else XI(pos_of_int (i lsr 1))
+    then Micromega_plugin.Micromega.XO(pos_of_int (i lsr 1))
+    else Micromega_plugin.Micromega.XI(pos_of_int (i lsr 1))
 
 let z_of_int i =
   if i = 0
-  then Z0
+  then Micromega_plugin.Micromega.Z0
   else
     if i > 0
-    then Zpos (pos_of_int i)
-    else Zneg (pos_of_int (-i))
+    then Micromega_plugin.Micromega.Zpos (pos_of_int i)
+    else Micromega_plugin.Micromega.Zneg (pos_of_int (-i))
 
 type my_tbl =
     {tbl:(hatom,int) Hashtbl.t; mutable count:int}
@@ -63,19 +62,19 @@ let create_tbl n = {tbl=Hashtbl.create n;count=1}
 let rec smt_Atom_to_micromega_pos ha =
   match Atom.atom ha with
   | Auop(UO_xO, ha) ->
-      Micromega.XO (smt_Atom_to_micromega_pos ha)
+      Micromega_plugin.Micromega.XO (smt_Atom_to_micromega_pos ha)
   | Auop(UO_xI, ha) ->
-      Micromega.XI (smt_Atom_to_micromega_pos ha)
-  | Acop CO_xH -> Micromega.XH
+      Micromega_plugin.Micromega.XI (smt_Atom_to_micromega_pos ha)
+  | Acop CO_xH -> Micromega_plugin.Micromega.XH
   | _ -> raise Not_found
 
 let smt_Atom_to_micromega_Z ha =
   match Atom.atom ha with
   | Auop(UO_Zpos, ha) ->
-      Micromega.Zpos (smt_Atom_to_micromega_pos ha)
+      Micromega_plugin.Micromega.Zpos (smt_Atom_to_micromega_pos ha)
   | Auop(UO_Zneg, ha) ->
-      Micromega.Zneg (smt_Atom_to_micromega_pos ha)
-  | Acop CO_Z0 -> Micromega.Z0
+      Micromega_plugin.Micromega.Zneg (smt_Atom_to_micromega_pos ha)
+  | Acop CO_Z0 -> Micromega_plugin.Micromega.Z0
   | _ -> raise Not_found
 
 let rec smt_Atom_to_micromega_pExpr tbl ha =
@@ -83,23 +82,23 @@ let rec smt_Atom_to_micromega_pExpr tbl ha =
   | Abop (BO_Zplus, ha, hb) ->
       let a = smt_Atom_to_micromega_pExpr tbl ha in
       let b = smt_Atom_to_micromega_pExpr tbl hb in
-      PEadd(a, b)
+      Micromega_plugin.Micromega.PEadd(a, b)
   | Abop (BO_Zmult, ha, hb) ->
       let a = smt_Atom_to_micromega_pExpr tbl ha in
       let b = smt_Atom_to_micromega_pExpr tbl hb in
-      PEmul(a, b)
+      Micromega_plugin.Micromega.PEmul(a, b)
   | Abop (BO_Zminus, ha, hb) ->
       let a = smt_Atom_to_micromega_pExpr tbl ha in
       let b = smt_Atom_to_micromega_pExpr tbl hb in
-      PEsub(a, b)
+      Micromega_plugin.Micromega.PEsub(a, b)
   | Auop (UO_Zopp, ha) ->
       let a = smt_Atom_to_micromega_pExpr tbl ha in
-      PEopp a
+      Micromega_plugin.Micromega.PEopp a
   | _ ->
-      try PEc (smt_Atom_to_micromega_Z ha)
+      try Micromega_plugin.Micromega.PEc (smt_Atom_to_micromega_Z ha)
       with Not_found ->
 	let v = get_atom_var tbl ha in
-	PEX (pos_of_int v)
+	Micromega_plugin.Micromega.PEX (pos_of_int v)
 
 
 (* morphism for LIA proposition (=, >, ...) *)
@@ -107,28 +106,28 @@ let rec smt_Atom_to_micromega_pExpr tbl ha =
 let smt_binop_to_micromega_formula tbl op ha hb =
   let op =
     match op with
-    | BO_Zlt -> OpLt
-    | BO_Zle -> OpLe
-    | BO_Zge -> OpGe
-    | BO_Zgt -> OpGt
-    | BO_eq _ -> OpEq
-    | _ -> error
+    | BO_Zlt -> Micromega_plugin.Micromega.OpLt
+    | BO_Zle -> Micromega_plugin.Micromega.OpLe
+    | BO_Zge -> Micromega_plugin.Micromega.OpGe
+    | BO_Zgt -> Micromega_plugin.Micromega.OpGt
+    | BO_eq _ -> Micromega_plugin.Micromega.OpEq
+    | _ -> Structures.error
 	  "lia.ml: smt_binop_to_micromega_formula expecting a formula"
   in
   let lhs = smt_Atom_to_micromega_pExpr tbl ha in
   let rhs = smt_Atom_to_micromega_pExpr tbl hb in
-  {flhs = lhs; fop = op; frhs = rhs }
+  {Micromega_plugin.Micromega.flhs = lhs; Micromega_plugin.Micromega.fop = op; Micromega_plugin.Micromega.frhs = rhs }
 
 let rec 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
-    | _ -> error
+    | _ -> Structures.error
 	  "lia.ml: smt_Atom_to_micromega_formula was expecting an LIA formula"
 
 (* specialized fold *)
 
 let default_constr = mkInt 0
-let default_tag = Mutils.Tag.from 0
+let default_tag = Micromega_plugin.Mutils.Tag.from 0
 (* morphism for general formulas *)
 
 let binop_array g tbl op def t =
@@ -146,14 +145,14 @@ let rec smt_Form_to_coq_micromega_formula tbl l =
   let v =
     match Form.pform l with
       | Fatom ha ->
-	A (smt_Atom_to_micromega_formula tbl ha,
+	Micromega_plugin.Coq_micromega.A (smt_Atom_to_micromega_formula tbl ha,
 	   default_tag,default_constr)
-      | Fapp (Ftrue, _) -> TT
-      | Fapp (Ffalse, _) -> FF
-      | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> C (x,y)) TT l
-      | Fapp (For, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> D (x,y)) FF l
+      | Fapp (Ftrue, _) -> Micromega_plugin.Coq_micromega.TT
+      | Fapp (Ffalse, _) -> Micromega_plugin.Coq_micromega.FF
+      | Fapp (Fand, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Micromega_plugin.Coq_micromega.C (x,y)) Micromega_plugin.Coq_micromega.TT l
+      | Fapp (For, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Micromega_plugin.Coq_micromega.D (x,y)) Micromega_plugin.Coq_micromega.FF l
       | Fapp (Fxor, l) -> failwith "todo:Fxor"
-      | Fapp (Fimp, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> I (x,None,y)) TT l
+      | Fapp (Fimp, l) -> binop_array smt_Form_to_coq_micromega_formula tbl (fun x y -> Micromega_plugin.Coq_micromega.I (x,None,y)) Micromega_plugin.Coq_micromega.TT l
       | Fapp (Fiff, l) -> failwith "todo:Fiff"
       | Fapp (Fite, l) -> failwith "todo:Fite"
       | Fapp (Fnot2 _, l) ->
@@ -163,7 +162,7 @@ let rec smt_Form_to_coq_micromega_formula tbl l =
           smt_Form_to_coq_micromega_formula tbl l.(0)
   in
   if Form.is_pos l then v
-  else N(v)
+  else Micromega_plugin.Coq_micromega.N(v)
 
 let binop_list tbl op def l =
   match l with
@@ -199,11 +198,11 @@ let binop_list tbl op def l =
 
 
 let smt_clause_to_coq_micromega_formula tbl cl =
-  binop_list tbl (fun x y -> C(x,y)) TT (List.map Form.neg cl)
+  binop_list tbl (fun x y -> Micromega_plugin.Coq_micromega.C(x,y)) Micromega_plugin.Coq_micromega.TT (List.map Form.neg cl)
 
 (* call to micromega solver *)
 let build_lia_certif cl =
   let tbl = create_tbl 13 in
-  let f = I(smt_clause_to_coq_micromega_formula tbl cl, None, FF) in
-  tbl, f, tauto_lia f
+  let f = Micromega_plugin.Coq_micromega.I(smt_clause_to_coq_micromega_formula tbl cl, None, Micromega_plugin.Coq_micromega.FF) in
+  tbl, f, Micromega_plugin.Coq_micromega.tauto_lia f
 
diff --git a/src/spl/Operators.v b/src/spl/Operators.v
index f7e011b..c597fe9 100644
--- a/src/spl/Operators.v
+++ b/src/spl/Operators.v
@@ -20,7 +20,6 @@
 (* Add LoadPath "../lia" as SMTCoq.lia. *)
 Require Import List PArray Bool Int63 ZMicromega.
 Require Import Misc State SMT_terms.
-Require Lia.
 
 Local Open Scope array_scope.
 Local Open Scope int63_scope.
diff --git a/src/spl/Syntactic.v b/src/spl/Syntactic.v
index fba6657..7a52694 100644
--- a/src/spl/Syntactic.v
+++ b/src/spl/Syntactic.v
@@ -18,7 +18,6 @@
 
 Require Import List PArray Bool Int63 ZMicromega.
 Require Import Misc State SMT_terms.
-Require Lia.
 
 Local Open Scope array_scope.
 Local Open Scope int63_scope.
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index f39bff4..868a311 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -99,11 +99,11 @@ type 'hform rule =
     *)
 
   (* Linear arithmetic *)
-  | LiaMicromega of 'hform list * Certificate.Mc.zArithProof list
+  | LiaMicromega of 'hform list * Micromega_plugin.Certificate.Mc.zArithProof list
   | LiaDiseq of 'hform
 
   (* Arithmetic simplifications *)
-  | SplArith of 'hform clause * 'hform * Certificate.Mc.zArithProof list
+  | SplArith of 'hform clause * 'hform * Micromega_plugin.Certificate.Mc.zArithProof list
 
   (* Elimination of operators *)
   | SplDistinctElim of 'hform clause * 'hform
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 8f2fea8..1abea36 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -17,7 +17,6 @@
 open Util
 open SmtMisc
 open CoqTerms
-open Errors
 
 module type ATOM = 
   sig 
@@ -315,7 +314,7 @@ module Make (Atom:ATOM) =
               let l1 = mk_hform b1 in
               let l2 = mk_hform b2 in
               get reify (Fapp (Fimp, [|l1;l2|]))
-            | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for implb")
+            | _ -> Structures.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
@@ -324,7 +323,7 @@ module Make (Atom:ATOM) =
 		let l2 = mk_hform b2 in
 		let l3 = mk_hform b3 in
 		get reify (Fapp(Fite, [|l1;l2;l3|]))
-	    | _ -> error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
+	    | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
 	    end
 	| _ -> 
 	    let a = atom_of_coq  h in
@@ -336,7 +335,7 @@ module Make (Atom:ATOM) =
 	    let l1 = mk_hform b1 in
             let l2 = mk_hform b2 in
             get reify (f [|l1; l2|])
-	| _ ->  error "SmtForm.Form.of_coq: wrong number of arguments"
+	| _ ->  Structures.error "SmtForm.Form.of_coq: wrong number of arguments"
 	  
       and mk_fnot i args =
 	match args with
@@ -350,7 +349,7 @@ 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|]))
-	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
+	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
 	  
       and mk_fand acc args = 
 	match args with
@@ -362,7 +361,7 @@ module Make (Atom:ATOM) =
 	    else 
 	      let l1 = mk_hform t1 in
 	      get reify (Fapp(Fand, Array.of_list  (l1::l2::acc)))
-	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for andb" 
+	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb" 
 
       and mk_for acc args = 
 	match args with
@@ -374,7 +373,7 @@ module Make (Atom:ATOM) =
 	    else 
 	      let l1 = mk_hform t1 in
 	      get reify (Fapp(For, Array.of_list (l1::l2::acc)))
-	| _ -> error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
+	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
 
       let l = mk_hform c in
       l
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index 74d3170..c372310 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -324,12 +324,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 Coq_micromega.M.coq_proofTerm; Coq_micromega.dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Coq_micromega.M.coq_proofTerm|]) in
+          let c' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Micromega_plugin.Coq_micromega.M.coq_proofTerm; Micromega_plugin.Coq_micromega.dump_proof_term f; l|]) d (mklApp cnil [|Lazy.force Micromega_plugin.Coq_micromega.M.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 Coq_micromega.M.coq_proofTerm; Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Coq_micromega.M.coq_proofTerm|]) in
+          let l' = List.fold_right (fun f l -> mklApp ccons [|Lazy.force Micromega_plugin.Coq_micromega.M.coq_proofTerm; Micromega_plugin.Coq_micromega.dump_proof_term f; l|]) l (mklApp cnil [|Lazy.force Micromega_plugin.Coq_micromega.M.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|]
         | Hole (prem_id, concl) ->
diff --git a/src/versions/standard/Array/PArray_standard.v b/src/versions/standard/Array/PArray_standard.v
index 2cc8366..4bf5e7a 100644
--- a/src/versions/standard/Array/PArray_standard.v
+++ b/src/versions/standard/Array/PArray_standard.v
@@ -80,8 +80,6 @@ Notation "t '.[' i '<-' a ']'" := (set t i a) (at level 50) : array_scope.
 
 Local Open Scope array_scope.
 
-Set Vm Optimize.
-
 Definition max_array_length := 4194302%int31.
 
 (** Axioms *)
diff --git a/src/versions/standard/Make b/src/versions/standard/Make
index 3834ee0..7c4497e 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/Make
@@ -9,6 +9,8 @@
 ########################################################################
 ## To generate the Makefile:                                          ##
 ##   coq_makefile -f Make -o Makefile                                 ##
+## Suppress the "Makefile" target                                     ##
+
 ## Change the "all" target into:                                      ##
 ##   all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES)                   ##
 ## Change the "install-natdynlink" target: change CMXSFILES into CMXS and add the same thing for CMXA. ##
@@ -21,6 +23,7 @@
 
 -R . SMTCoq
 
+-I .
 -I cnf
 -I euf
 -I lia
@@ -32,19 +35,16 @@
 -I versions/standard/Int63
 -I versions/standard/Array
 
--custom "cd ../unit-tests; make" "" "test"
--custom "cd ../unit-tests; make zchaff" "" "ztest"
--custom "cd ../unit-tests; make verit" "" "vtest"
+-I $(COQBIN)../plugins/micromega
 
--custom "$(CAMLLEX) $<" "%.mll" "%.ml"
--custom "$(CAMLYACC) $<" "%.mly" "%.ml %.mli"
--custom "" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" "ml"
+# -extra "test" "" "cd ../unit-tests; make" ""
+# -extra "ztest" "" "cd ../unit-tests; make zchaff"
+# -extra "vtest" "" "cd ../unit-tests; make verit"
 
--custom "$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^" "versions/standard/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx" "$(CMXA)"
--custom "$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^" "$(CMXA)" "$(CMXS)"
+-extra "%.ml" "%.mll" "$(CAMLLEX) $<"
+-extra "%.ml %.mli" "%.mly" "$(CAMLYACC) $<"
+-extra-phony "smtcoq_plugin.mlpack.d" "verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml" ""
 
-CMXA = smtcoq.cmxa
-CMXS = smtcoq_plugin.cmxs
 CAMLLEX = $(CAMLBIN)ocamllex
 CAMLYACC = $(CAMLBIN)ocamlyacc
 
@@ -107,4 +107,5 @@ SMT_terms.v
 State.v
 Trace.v
 
-smtcoq_plugin.ml4
+g_smtcoq.ml4
+smtcoq_plugin.mlpack
diff --git a/src/versions/standard/Makefile b/src/versions/standard/Makefile
index 43946bf..9fda4ea 100644
--- a/src/versions/standard/Makefile
+++ b/src/versions/standard/Makefile
@@ -2,7 +2,7 @@
 ##  v      #                   The Coq Proof Assistant                     ##
 ## <O___,, #                INRIA - CNRS - LIX - LRI - PPS                 ##
 ##   \VV/  #                                                               ##
-##    //   #  Makefile automagically generated by coq_makefile V8.5pl2     ##
+##    //   #  Makefile automagically generated by coq_makefile V8.6.1      ##
 #############################################################################
 
 # WARNING
@@ -25,6 +25,11 @@
 # TIMED if non empty, use the default time command as TIMECMD;
 # ZDEBUG/COQDEBUG to specify debug flags for ocamlc&ocamlopt/coqc;
 # DSTROOT to specify a prefix to install path.
+# VERBOSE to disable the short display of compilation rules.
+
+VERBOSE?=
+SHOW := $(if $(VERBOSE),@true "",@echo "")
+HIDE := $(if $(VERBOSE),,@)
 
 # Here is a hack to make $(eval $(shell works:
 define donewline
@@ -34,8 +39,8 @@ endef
 includecmdwithout@ = $(eval $(subst @,$(donewline),$(shell { $(1) | tr -d '\r' | tr '\n' '@'; })))
 $(call includecmdwithout@,$(COQBIN)coqtop -config)
 
-TIMED=
-TIMECMD=
+TIMED?=
+TIMECMD?=
 STDTIME?=/usr/bin/time -f "$* (user: %U mem: %M ko)"
 TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD))
 
@@ -49,7 +54,8 @@ vo_to_obj = $(addsuffix .o,\
 #                        #
 ##########################
 
-OCAMLLIBS?=-I "cnf"\
+OCAMLLIBS?=-I "."\
+  -I "cnf"\
   -I "euf"\
   -I "lia"\
   -I "smtlib2"\
@@ -58,9 +64,11 @@ OCAMLLIBS?=-I "cnf"\
   -I "zchaff"\
   -I "versions/standard"\
   -I "versions/standard/Int63"\
-  -I "versions/standard/Array"
+  -I "versions/standard/Array"\
+  -I "$(COQBIN)../plugins/micromega"
 COQLIBS?=\
   -R "." SMTCoq\
+  -I "."\
   -I "cnf"\
   -I "euf"\
   -I "lia"\
@@ -70,7 +78,8 @@ COQLIBS?=\
   -I "zchaff"\
   -I "versions/standard"\
   -I "versions/standard/Int63"\
-  -I "versions/standard/Array"
+  -I "versions/standard/Array"\
+  -I "$(COQBIN)../plugins/micromega"
 COQCHKLIBS?=\
   -R "." SMTCoq
 COQDOCLIBS?=\
@@ -82,8 +91,6 @@ COQDOCLIBS?=\
 #                        #
 ##########################
 
-CMXA=smtcoq.cmxa
-CMXS=smtcoq_plugin.cmxs
 CAMLLEX=$(CAMLBIN)ocamllex
 CAMLYACC=$(CAMLBIN)ocamlyacc
 
@@ -109,10 +116,13 @@ COQSRCLIBS?=-I "$(COQLIB)kernel" \
 -I "$(COQLIB)proofs" \
 -I "$(COQLIB)tactics" \
 -I "$(COQLIB)tools" \
+-I "$(COQLIB)ltacprof" \
 -I "$(COQLIB)toplevel" \
 -I "$(COQLIB)stm" \
 -I "$(COQLIB)grammar" \
 -I "$(COQLIB)config" \
+-I "$(COQLIB)ltac" \
+-I "$(COQLIB)engine" \
  \
   -I "$(COQLIB)/plugins/btauto" \
   -I "$(COQLIB)/plugins/cc" \
@@ -122,6 +132,7 @@ COQSRCLIBS?=-I "$(COQLIB)kernel" \
   -I "$(COQLIB)/plugins/firstorder" \
   -I "$(COQLIB)/plugins/fourier" \
   -I "$(COQLIB)/plugins/funind" \
+  -I "$(COQLIB)/plugins/ltac" \
   -I "$(COQLIB)/plugins/micromega" \
   -I "$(COQLIB)/plugins/nsatz" \
   -I "$(COQLIB)/plugins/omega" \
@@ -129,21 +140,24 @@ COQSRCLIBS?=-I "$(COQLIB)kernel" \
   -I "$(COQLIB)/plugins/romega" \
   -I "$(COQLIB)/plugins/rtauto" \
   -I "$(COQLIB)/plugins/setoid_ring" \
+  -I "$(COQLIB)/plugins/ssrmatching" \
   -I "$(COQLIB)/plugins/syntax" \
   -I "$(COQLIB)/plugins/xml"
 ZFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB)
 
-CAMLC?=$(OCAMLC) -c -rectypes -thread
-CAMLOPTC?=$(OCAMLOPT) -c -rectypes -thread
-CAMLLINK?=$(OCAMLC) -rectypes -thread
-CAMLOPTLINK?=$(OCAMLOPT) -rectypes -thread
+CAMLC?=$(OCAMLFIND) ocamlc -c -rectypes -thread
+CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread
+CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread
+CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread
+CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack
+CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)
 GRAMMARS?=grammar.cma
 ifeq ($(CAMLP4),camlp5)
-CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma
+CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
 else
-CAMLP4EXTEND=threads.cma
+CAMLP4EXTEND=
 endif
-PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \
+PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(COQLIB)/grammar compat5.cmo \
   $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'
 
 ##################
@@ -207,7 +221,7 @@ GHTMLFILES:=$(VFILES:.v=.g.html)
 OBJFILES=$(call vo_to_obj,$(VOFILES))
 ALLNATIVEFILES=$(OBJFILES:.o=.cmi) $(OBJFILES:.o=.cmo) $(OBJFILES:.o=.cmx) $(OBJFILES:.o=.cmxs)
 NATIVEFILES=$(foreach f, $(ALLNATIVEFILES), $(wildcard $f))
-ML4FILES:=smtcoq_plugin.ml4
+ML4FILES:=g_smtcoq.ml4
 
 ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
 -include $(addsuffix .d,$(ML4FILES))
@@ -254,6 +268,18 @@ endif
 
 .SECONDARY: $(addsuffix .d,$(MLFILES))
 
+MLPACKFILES:=smtcoq_plugin.mlpack
+
+ifneq ($(filter-out archclean clean cleanall printenv,$(MAKECMDGOALS)),)
+-include $(addsuffix .d,$(MLPACKFILES))
+else
+ifeq ($(MAKECMDGOALS),)
+-include $(addsuffix .d,$(MLPACKFILES))
+endif
+endif
+
+.SECONDARY: $(addsuffix .d,$(MLPACKFILES))
+
 MLIFILES:=trace/smtAtom.mli\
   trace/smtForm.mli\
   smtlib2/smtlib2_parse.mli\
@@ -270,7 +296,7 @@ endif
 
 .SECONDARY: $(addsuffix .d,$(MLIFILES))
 
-ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo)
+ALLCMOFILES:=$(ML4FILES:.ml4=.cmo) $(MLFILES:.ml=.cmo) $(MLPACKFILES:.mlpack=.cmo)
 CMOFILES=$(filter-out $(addsuffix .cmo,$(foreach lib,$(MLLIBFILES:.mllib=_MLLIB_DEPENDENCIES) $(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ALLCMOFILES))
 CMXFILES=$(CMOFILES:.cmo=.cmx)
 OFILES=$(CMXFILES:.cmx=.o)
@@ -288,14 +314,14 @@ endif
 #                                     #
 #######################################
 
-all: ml $(CMXFILES) $(CMXA) $(CMXS) $(VOFILES)
+all: $(VOFILES) $(CMOFILES) $(if $(HASNATDYNLINK_OR_EMPTY),$(CMXSFILES)) 
 
 mlihtml: $(MLIFILES:.mli=.cmi)
 	 mkdir $@ || rm -rf $@/*
-	$(OCAMLDOC) -html -rectypes -d $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
+	$(OCAMLFIND) 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)
+	$(OCAMLFIND) ocamldoc -latex -rectypes -o $@ -m A $(ZDEBUG) $(ZFLAGS) $(^:.cmi=.mli)
 
 quick: $(VOFILES:.vo=.vio)
 
@@ -333,7 +359,7 @@ beautify: $(VFILES:=.beautified)
 	@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 archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo
+.PHONY: all archclean beautify byte clean cleanall gallina gallinahtml html install install-doc install-natdynlink install-toploop opt printenv quick uninstall userinstall validate vio2vo smtcoq_plugin.mlpack.d
 
 ###################
 #                 #
@@ -341,28 +367,27 @@ beautify: $(VFILES:=.beautified)
 #                 #
 ###################
 
-test: 
-	cd ../unit-tests; make
-
-ztest: 
-	cd ../unit-tests; make zchaff
-
-vtest: 
-	cd ../unit-tests; make verit
-
 %.ml: %.mll
 	$(CAMLLEX) $<
 
 %.ml %.mli: %.mly
 	$(CAMLYACC) $<
 
-ml: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml
+smtcoq_plugin.mlpack.d: verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml
+
+#####################################
+#                                   #
+# Ad-hoc implicit rules for mlpack. #
+#                                   #
+#####################################
 
-$(CMXA): versions/standard/structures.cmx trace/smtMisc.cmx trace/coqTerms.cmx trace/smtForm.cmx trace/smtCertif.cmx trace/smtTrace.cmx trace/smtCnf.cmx trace/satAtom.cmx trace/smtAtom.cmx zchaff/satParser.cmx zchaff/zchaffParser.cmx zchaff/cnfParser.cmx zchaff/zchaff.cmx smtlib2/smtlib2_util.cmx smtlib2/smtlib2_ast.cmx smtlib2/smtlib2_parse.cmx smtlib2/smtlib2_lex.cmx lia/lia.cmx verit/veritSyntax.cmx verit/veritParser.cmx verit/veritLexer.cmx smtlib2/smtlib2_genConstr.cmx trace/smtCommands.cmx verit/verit.cmx smtcoq_plugin.cmx
-	$(CAMLOPTLINK) $(ZFLAGS) -a -o $@ $^
+$(addsuffix .cmx,$(filter $(basename $(MLFILES)),$(smtcoq_plugin_MLPACK_DEPENDENCIES))): %.cmx: %.ml
+	$(SHOW)'CAMLOPT -c -for-pack Smtcoq_plugin $<'
+	$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack Smtcoq_plugin $<
 
-$(CMXS): $(CMXA)
-	$(CAMLOPTLINK) $(ZFLAGS) -o $@ -linkall -shared $^
+$(addsuffix .cmx,$(filter $(basename $(ML4FILES)),$(smtcoq_plugin_MLPACK_DEPENDENCIES))): %.cmx: %.ml4
+	$(SHOW)'CAMLOPT -c -pp -for-pack Smtcoq_plugin $<'
+	$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) -for-pack Smtcoq_plugin $(PP) -impl $<
 
 ####################
 #                  #
@@ -380,11 +405,7 @@ userinstall:
 	+$(MAKE) USERINSTALL=true install
 
 install-natdynlink:
-	cd "." && for i in $(CMXS); do \
-	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \
-	 install -m 0755 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \
-	done
-	cd "." && for i in $(CMXA); do \
+	cd "." && for i in $(CMXSFILES); do \
 	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \
 	 install -m 0755 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \
 	done
@@ -394,7 +415,7 @@ install-toploop: $(MLLIBFILES:.mllib=.cmxs)
 	 install -m 0755 $?  "$(DSTROOT)"$(COQTOPINSTALL)/
 
 install:$(if $(HASNATDYNLINK_OR_EMPTY),install-natdynlink)
-	cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMXFILES) $(CMIFILES) $(CMAFILES); do \
+	cd "." && for i in $(VOFILES) $(VFILES) $(GLOBFILES) $(NATIVEFILES) $(CMOFILES) $(CMIFILES) $(CMAFILES); do \
 	 install -d "`dirname "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i`"; \
 	 install -m 0644 $$i "$(DSTROOT)"$(COQLIBINSTALL)/SMTCoq/$$i; \
 	done
@@ -426,21 +447,26 @@ uninstall: uninstall_me.sh
 
 .merlin:
 	@echo 'FLG -rectypes' > .merlin
-	@echo "B $(COQLIB) kernel" >> .merlin
-	@echo "B $(COQLIB) lib" >> .merlin
-	@echo "B $(COQLIB) library" >> .merlin
-	@echo "B $(COQLIB) parsing" >> .merlin
-	@echo "B $(COQLIB) pretyping" >> .merlin
-	@echo "B $(COQLIB) interp" >> .merlin
-	@echo "B $(COQLIB) printing" >> .merlin
-	@echo "B $(COQLIB) intf" >> .merlin
-	@echo "B $(COQLIB) proofs" >> .merlin
-	@echo "B $(COQLIB) tactics" >> .merlin
-	@echo "B $(COQLIB) tools" >> .merlin
-	@echo "B $(COQLIB) toplevel" >> .merlin
-	@echo "B $(COQLIB) stm" >> .merlin
-	@echo "B $(COQLIB) grammar" >> .merlin
-	@echo "B $(COQLIB) config" >> .merlin
+	@echo "B $(COQLIB)kernel" >> .merlin
+	@echo "B $(COQLIB)lib" >> .merlin
+	@echo "B $(COQLIB)library" >> .merlin
+	@echo "B $(COQLIB)parsing" >> .merlin
+	@echo "B $(COQLIB)pretyping" >> .merlin
+	@echo "B $(COQLIB)interp" >> .merlin
+	@echo "B $(COQLIB)printing" >> .merlin
+	@echo "B $(COQLIB)intf" >> .merlin
+	@echo "B $(COQLIB)proofs" >> .merlin
+	@echo "B $(COQLIB)tactics" >> .merlin
+	@echo "B $(COQLIB)tools" >> .merlin
+	@echo "B $(COQLIB)ltacprof" >> .merlin
+	@echo "B $(COQLIB)toplevel" >> .merlin
+	@echo "B $(COQLIB)stm" >> .merlin
+	@echo "B $(COQLIB)grammar" >> .merlin
+	@echo "B $(COQLIB)config" >> .merlin
+	@echo "B $(COQLIB)ltac" >> .merlin
+	@echo "B $(COQLIB)engine" >> .merlin
+	@echo "B /home/artemis/Recherche/Github/smtcoq/smtcoq/src/versions/standard" >> .merlin
+	@echo "S /home/artemis/Recherche/Github/smtcoq/smtcoq/src/versions/standard" >> .merlin
 	@echo "B cnf" >> .merlin
 	@echo "S cnf" >> .merlin
 	@echo "B euf" >> .merlin
@@ -461,6 +487,8 @@ uninstall: uninstall_me.sh
 	@echo "S versions/standard/Int63" >> .merlin
 	@echo "B versions/standard/Array" >> .merlin
 	@echo "S versions/standard/Array" >> .merlin
+	@echo "B $(COQBIN)../plugins/micromega" >> .merlin
+	@echo "S $(COQBIN)../plugins/micromega" >> .merlin
 
 clean::
 	rm -f $(ALLCMOFILES) $(CMIFILES) $(CMAFILES)
@@ -471,30 +499,23 @@ clean::
 	rm -f $(VOFILES) $(VOFILES:.vo=.vio) $(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 uninstall_me.sh
-	- rm -rf test
-	- rm -rf ztest
-	- rm -rf vtest
-	- rm -rf ml
-	- rm -rf $(CMXA)
-	- rm -rf $(CMXS)
-	- rm -f ../unit-tests/*.vo ../unit-tests/*.zlog ../unit-tests/*.vtlog verit/veritParser.mli verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.mli smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtcoq.a
 
 cleanall:: clean
-	rm -f $(patsubst %.v,.%.aux,$(VFILES))
+	rm -f $(foreach f,$(VFILES:.v=),$(dir $(f)).$(notdir $(f)).aux)
 
 archclean::
 	rm -f *.cmx *.o
 
 printenv:
 	@"$(COQBIN)coqtop" -config
-	@echo 'CAMLC =	$(CAMLC)'
-	@echo 'CAMLOPTC =	$(CAMLOPTC)'
+	@echo 'OCAMLFIND =	$(OCAMLFIND)'
 	@echo 'PP =	$(PP)'
 	@echo 'COQFLAGS =	$(COQFLAGS)'
 	@echo 'COQLIBINSTALL =	$(COQLIBINSTALL)'
 	@echo 'COQDOCINSTALL =	$(COQDOCINSTALL)'
 
 
+
 ###################
 #                 #
 # Implicit rules. #
@@ -502,34 +523,60 @@ printenv:
 ###################
 
 $(MLIFILES:.mli=.cmi): %.cmi: %.mli
-	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
+	$(SHOW)'CAMLC -c $<'
+	$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
 
 $(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli
-	$(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 $(ML4FILES:.ml4=.cmo): %.cmo: %.ml4
-	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
+	$(SHOW)'CAMLC -pp -c $<'
+	$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
 
 $(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4
-	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
+	$(SHOW)'CAMLOPT -pp -c $<'
+	$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<
 
 $(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4
-	$(OCAMLDEP) -slash $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+	$(SHOW)'CAMLDEP -pp $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 $(MLFILES:.ml=.cmo): %.cmo: %.ml
-	$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
+	$(SHOW)'CAMLC -c $<'
+	$(HIDE)$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<
 
 $(filter-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml
-	$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<
+	$(SHOW)'CAMLOPT -c $<'
+	$(HIDE)$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<
 
 $(addsuffix .d,$(MLFILES)): %.ml.d: %.ml
-	$(OCAMLDEP) -slash $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+	$(SHOW)'CAMLDEP $<'
+	$(HIDE)$(CAMLDEP) $(OCAMLLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+
+$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx
+	$(SHOW)'CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<
 
 $(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa
-	$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<
+	$(SHOW)'CAMLOPT -shared -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<
+
+$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack
+	$(SHOW)'CAMLC -pack -o $@'
+	$(HIDE)$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^
+
+$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack
+	$(SHOW)'CAMLOPT -pack -o $@'
+	$(HIDE)$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^
+
+$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(OCAMLLIBS) -c "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 $(VOFILES): %.vo: %.v
-	$(COQC) $(COQDEBUG) $(COQFLAGS) $<
+	$(SHOW)COQC $<
+	$(HIDE)$(COQC) $(COQDEBUG) $(COQFLAGS) $<
 
 $(GLOBFILES): %.glob: %.v
 	$(COQC) $(COQDEBUG) $(COQFLAGS) $<
@@ -553,7 +600,8 @@ $(GHTMLFILES): %.g.html: %.v %.glob
 	$(COQDOC) $(COQDOCFLAGS)  -html -g $< -o $@
 
 $(addsuffix .d,$(VFILES)): %.v.d: %.v
-	$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
+	$(SHOW)'COQDEP $<'
+	$(HIDE)$(COQDEP) $(COQLIBS) "$<" > "$@" || ( RV=$$?; rm -f "$@"; exit $${RV} )
 
 $(addsuffix .beautified,$(VFILES)): %.v.beautified:
 	$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v
diff --git a/src/versions/standard/g_smtcoq_standard.ml4 b/src/versions/standard/g_smtcoq_standard.ml4
new file mode 100644
index 0000000..ab097a1
--- /dev/null
+++ b/src/versions/standard/g_smtcoq_standard.ml4
@@ -0,0 +1,62 @@
+(**************************************************************************)
+(*                                                                        *)
+(*     SMTCoq                                                             *)
+(*     Copyright (C) 2011 - 2016                                          *)
+(*                                                                        *)
+(*     Michaël Armand                                                     *)
+(*     Benjamin Grégoire                                                  *)
+(*     Chantal Keller                                                     *)
+(*                                                                        *)
+(*     Inria - École Polytechnique - Université Paris-Sud                 *)
+(*                                                                        *)
+(*   This file is distributed under the terms of the CeCILL-C licence     *)
+(*                                                                        *)
+(**************************************************************************)
+
+
+DECLARE PLUGIN "smtcoq_plugin"
+
+open Genarg
+open Stdarg
+open Constrarg
+
+VERNAC COMMAND EXTEND Vernac_zchaff CLASSIFIED AS QUERY
+| [ "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_verit CLASSIFIED AS QUERY
+| [ "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_Theorem" ident(name) string(fsmt) string(fproof) ] ->
+  [
+    Verit.theorem name fsmt fproof
+  ]
+END
+
+
+TACTIC EXTEND Tactic_zchaff
+| [ "zchaff" ] -> [ Zchaff.tactic () ]
+END
+
+TACTIC EXTEND Tactic_verit
+| [ "verit" ] -> [ Verit.tactic () ]
+END
diff --git a/src/versions/standard/smtcoq_plugin_standard.ml4 b/src/versions/standard/smtcoq_plugin_standard.ml4
index 6ae3545..ab097a1 100644
--- a/src/versions/standard/smtcoq_plugin_standard.ml4
+++ b/src/versions/standard/smtcoq_plugin_standard.ml4
@@ -16,7 +16,11 @@
 
 DECLARE PLUGIN "smtcoq_plugin"
 
-VERNAC COMMAND EXTEND Vernac_zchaff
+open Genarg
+open Stdarg
+open Constrarg
+
+VERNAC COMMAND EXTEND Vernac_zchaff CLASSIFIED AS QUERY
 | [ "Parse_certif_zchaff" 
     ident(dimacs) ident(trace) string(fdimacs) string(fproof) ] ->
   [
@@ -32,7 +36,7 @@ VERNAC COMMAND EXTEND Vernac_zchaff
   ]
 END
 
-VERNAC COMMAND EXTEND Vernac_verit
+VERNAC COMMAND EXTEND Vernac_verit CLASSIFIED AS QUERY
 | [ "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) ] ->
   [
diff --git a/src/versions/standard/smtcoq_plugin_standard.mlpack b/src/versions/standard/smtcoq_plugin_standard.mlpack
new file mode 100644
index 0000000..3ab358b
--- /dev/null
+++ b/src/versions/standard/smtcoq_plugin_standard.mlpack
@@ -0,0 +1,34 @@
+Structures
+
+SmtMisc
+CoqTerms
+SmtForm
+SmtCertif
+SmtTrace
+SmtCnf
+SatAtom
+SmtAtom
+
+SatParser
+ZchaffParser
+CnfParser
+Zchaff
+
+Smtlib2_util
+Smtlib2_ast
+Smtlib2_parse
+Smtlib2_lex
+
+Lia
+
+VeritSyntax
+VeritParser
+VeritLexer
+
+Smtlib2_genConstr
+
+SmtCommands
+
+Verit
+
+G_smtcoq
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index 19104fe..45a8ca4 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -111,7 +111,7 @@ let mkTConst c noc ty =
     const_entry_opaque      = false;
     const_entry_inline_code = false }
 
-let error = Errors.error
+let error = CErrors.error
 
 let coqtype = Future.from_val Term.mkSet
 
@@ -138,14 +138,15 @@ let lift = Vars.lift
 let tclTHEN = Tacticals.New.tclTHEN
 let tclTHENLAST = Tacticals.New.tclTHENLAST
 let assert_before = Tactics.assert_before
-let vm_cast_no_check t = Proofview.V82.tactic (Tactics.vm_cast_no_check t)
+let vm_cast_no_check t = Tactics.vm_cast_no_check t
+(* let vm_cast_no_check t = Proofview.V82.tactic (Tactics.vm_cast_no_check t) *)
 let mk_tactic tac =
-  Proofview.Goal.nf_enter (fun gl ->
+  Proofview.Goal.nf_enter {enter = (fun gl ->
     let env = Proofview.Goal.env gl in
-    let sigma = Proofview.Goal.sigma gl in
+    let sigma = Tacmach.New.project gl in
     let t = Proofview.Goal.concl gl in
     tac env sigma t
-  )
+  )}
 let set_evars_tac noc =
   mk_tactic (
       fun env sigma _ ->