V8.9 (#43)

* New syntax for implicit arguments

* Towards 8.9: problems with Micromega plugin

* Move to _CoqProject

* Back to name Makefile

* Switch to Makefile.local instead of -extra

* The compilation issue is a Coq bug

* Ok with 8.9

* INSTALL with 8.9

* Everything ok with 8.9

19 files changed, 2746 insertions, 57 deletions

diff --git a/.gitignore b/.gitignore
index b5aaccd..e232f6a 100644
--- a/.gitignore
+++ b/.gitignore
@@ -21,9 +21,10 @@ setup.log
 .nia.cache
 
 # cp targets of src/configure.sh:
-src/Make
+src/_CoqProject
 src/Makefile
 src/Makefile.conf
+src/Makefile.local
 src/smtcoq_plugin.ml4
 src/versions/native/Structures.v
 src/g_smtcoq.ml4
diff --git a/INSTALL.md b/INSTALL.md
index 7801493..5ad4ecb 100644
--- a/INSTALL.md
+++ b/INSTALL.md
@@ -15,7 +15,7 @@ changes](#setting-up-environment-for-smtcoq).
 
 ## Requirements
 
-You need to have OCaml version >= 4.04.0 and Coq version 8.8.*.
+You need to have OCaml version >= 4.04.0 and Coq version 8.9.0.
 The easiest way to install these two pieces of software is through opam.
 
 > **Warning**: The version of Coq that you plan to use must have been compiled
@@ -26,7 +26,7 @@ The easiest way to install these two pieces of software is through opam.
 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.8.
+Coq-8.9.
 
 
 ### Installation with Coq and OCaml opam packages
@@ -63,16 +63,16 @@ opam switch 4.04.0
 
 #### Install Coq
 
-After OCaml is installed, you can install Coq through opam (we recommend 8.8.2).
+After OCaml is installed, you can install Coq-8.9.0 through opam.
 
 ```bash
-opam install coq.8.8.2
+opam install coq.8.9.0
 ```
 
 If you also want to install CoqIDE at the same time you can do
 
 ```bash
-opam install coq.8.8.2 coqide.8.8.2
+opam install coq.8.9.0 coqide.8.9.0
 ```
 
 but you might need to install some extra packages and libraries for your system
@@ -90,11 +90,11 @@ make install
 ```
 
 
-### Installation with official Coq 8.8 release
+### Installation with official Coq 8.9 release
 
-1. Download the last stable version of Coq 8.8:
+1. Download the last stable version of Coq 8.9:
 ```bash
-wget https://github.com/coq/coq/archive/V8.8.2.tar.gz
+wget https://github.com/coq/coq/archive/V8.9.0.tar.gz
 ```
    and compile it by following the instructions available in the
    repository (make sure you use OCaml 4.04.0 for that). We recommand
@@ -107,7 +107,7 @@ make
 2. Set an environment variable COQBIN to the directory where Coq's
    binaries are; for instance:
 ```bash
-export COQBIN=/home/jdoe/coq-8.8.2/bin/
+export COQBIN=/home/jdoe/coq-8.9.0/bin/
 ```
    (the final slash is mandatory).
 
diff --git a/src/Misc.v b/src/Misc.v
index 5fc6602..b675599 100644
--- a/src/Misc.v
+++ b/src/Misc.v
@@ -996,7 +996,7 @@ Section Forall2.
 
 End Forall2.
 
-Implicit Arguments forallb2 [A B].
+Arguments forallb2 {A B} f l1 l2.
 
 
 (* Compatibility between native-coq and Coq 8.5 *)
diff --git a/src/SMT_terms.v b/src/SMT_terms.v
index 169c761..a85804c 100644
--- a/src/SMT_terms.v
+++ b/src/SMT_terms.v
@@ -489,8 +489,8 @@ Module Typ.
     | Cast (k: forall P, P A -> P B)
     | NoCast.
 
-    Implicit Arguments Cast [A B].
-    Implicit Arguments NoCast [A B].
+    Arguments Cast {A B} k.
+    Arguments NoCast {A B}.
 
     Notation idcast := (Cast (fun P x => x)).
     (* La fonction cast calcule cast_result *)
diff --git a/src/Trace.v b/src/Trace.v
index 4d832de..e7c7d22 100644
--- a/src/Trace.v
+++ b/src/Trace.v
@@ -528,7 +528,7 @@ Inductive step :=
     Form.check_form t_form && Atom.check_atom t_atom &&
     Atom.wt t_i t_func t_atom &&
     euf_checker (* t_atom t_form *) C.is_false (add_roots (S.make nclauses) d used_roots) t confl.
-  Implicit Arguments checker [].
+  Arguments checker d used_roots c : clear implicits.
 
 
   Definition setup_checker_step_debug d used_roots (c:certif) :=
@@ -772,3 +772,10 @@ End Euf_Checker.
 
 
 Unset Implicit Arguments.
+
+
+(*
+   Local Variables:
+   coq-load-path: ((rec "." "SMTCoq"))
+   End:
+*)
diff --git a/src/configure.sh b/src/configure.sh
index 85571cd..3def21c 100755
--- a/src/configure.sh
+++ b/src/configure.sh
@@ -2,9 +2,10 @@
 
 pre=$(echo $0 | sed "s,\(\([^/]*/\)*\)[^/]*,\1,")
 
-rm -f ${pre}Make
+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.ml4
@@ -23,7 +24,8 @@ if [ $@ -a $@ = -native ]; then
     cp ${pre}versions/native/smtcoq_plugin_native.ml4 ${pre}smtcoq_plugin.ml4
     cp ${pre}versions/native/Structures_native.v ${pre}versions/native/Structures.v
 else
-    cp ${pre}versions/standard/Make ${pre}Make
+    cp ${pre}versions/standard/_CoqProject ${pre}_CoqProject
+    cp ${pre}versions/standard/Makefile.local ${pre}Makefile.local
     cp ${pre}versions/standard/g_smtcoq_standard.ml4 ${pre}g_smtcoq.ml4
     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
@@ -33,6 +35,5 @@ else
     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
-    coq_makefile -f Make -o Makefile
-    sed -i Makefile -e "s/ocamldep/ocamldep -native/" -e "s/	\$(HIDE)\$(MAKE) --no-print-directory -f \"\$(SELF)\" post-all//"
+    coq_makefile -f _CoqProject -o Makefile
 fi
diff --git a/src/lia/lia.ml b/src/lia/lia.ml
index d8ed560..d546559 100644
--- a/src/lia/lia.ml
+++ b/src/lia/lia.ml
@@ -193,6 +193,15 @@ 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)
 
+(* backported from Coq-8.8.2 *)
+(* val tauto_lia : Mc.z formula -> Certificate.Mc.zArithProof list option *)
+let tauto_lia ff =
+  let prover = linear_Z in
+  let cnf_ff,_ = cnf Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce  ff in
+  match witness_list_tags [prover] cnf_ff with
+    | None -> None
+    | Some l -> Some (List.map fst l)
+
 (* call to micromega solver *)
 let build_lia_certif cl =
   let tbl = create_tbl 13 in
diff --git a/src/trace/smtCertif.ml b/src/trace/smtCertif.ml
index 6ce6997..27b56c3 100644
--- a/src/trace/smtCertif.ml
+++ b/src/trace/smtCertif.ml
@@ -324,7 +324,7 @@ let to_string r =
 
 
 (* To use <print_certif>, pass, as first and second argument, <Form.to_smt> and <Atom.to_string> *)
-let print_certif form_to_smt atom_to_string c where=
+let print_certif form_to_smt atom_to_string c where =
   let rec start c =
     match c.prev with
     | None -> c
diff --git a/src/trace/smtCertif.mli b/src/trace/smtCertif.mli
index 6a145bb..3f65930 100644
--- a/src/trace/smtCertif.mli
+++ b/src/trace/smtCertif.mli
@@ -239,4 +239,4 @@ and 'hform resolution = {
 }
 val used_clauses : 'a rule -> 'a clause list
 val to_string : 'a clause_kind -> string
-val print_certif : ('a -> Format.formatter -> 'b -> 'c) -> 'a -> 'b clause -> string -> unit
+val print_certif : ('a -> Format.formatter -> 'b -> unit) -> 'a -> 'b clause -> string -> unit
diff --git a/src/versions/native/structures.ml b/src/versions/native/structures.ml
index e11697e..ee4bf96 100644
--- a/src/versions/native/structures.ml
+++ b/src/versions/native/structures.ml
@@ -139,10 +139,10 @@ let mkTrace step_to_coq next carray _ _ _ _ size step def_step r =
 
 
 (* Micromega *)
-module Micromega_plugin_Certificate = Certificate
-module Micromega_plugin_Coq_micromega = Coq_micromega
 module Micromega_plugin_Micromega = Micromega
 module Micromega_plugin_Mutils = Mutils
+module Micromega_plugin_Certificate = Certificate
+module Micromega_plugin_Coq_micromega = Coq_micromega
 
 let micromega_coq_proofTerm =
   Coq_micromega.M.coq_proofTerm
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli
index cae581e..939ffc7 100644
--- a/src/versions/native/structures.mli
+++ b/src/versions/native/structures.mli
@@ -81,10 +81,10 @@ val mkTrace :
 
 
 (* Micromega *)
-module Micromega_plugin_Certificate = Certificate
-module Micromega_plugin_Coq_micromega = Coq_micromega
 module Micromega_plugin_Micromega = Micromega
 module Micromega_plugin_Mutils = Mutils
+module Micromega_plugin_Certificate = Certificate
+module Micromega_plugin_Coq_micromega = Coq_micromega
 
 val micromega_coq_proofTerm : constr lazy_t
 val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr
@@ -107,7 +107,7 @@ val set_evars_tac : 'a -> Proof_type.tactic
 type constr_expr = Topconstr.constr_expr
 val error : string -> 'a
 val extern_constr : constr -> Topconstr.constr_expr
-val destruct_rel_decl : Term.rel_declaration -> name * constr
+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
diff --git a/src/versions/standard/Makefile.local b/src/versions/standard/Makefile.local
new file mode 100644
index 0000000..67b0b8e
--- /dev/null
+++ b/src/versions/standard/Makefile.local
@@ -0,0 +1,33 @@
+########################################################################
+##   This file is intended to developers: please do not use it        ##
+## directly, rather use the "configure.sh" script.                    ##
+########################################################################
+
+
+test :
+	cd ../unit-tests; make
+
+ztest :
+	cd ../unit-tests; make zchaff
+
+vtest :
+	cd ../unit-tests; make verit
+
+lfsctest :
+	cd ../unit-tests; make lfsc
+
+clean::
+	cd ../unit-tests; make clean; rm *vo *glob
+
+
+CAMLLEX = $(CAMLBIN)ocamllex
+CAMLYACC = $(CAMLBIN)ocamlyacc
+
+%.ml :  %.mll
+	$(CAMLLEX) $<
+
+%.ml %.mli :  %.mly
+	$(CAMLYACC) $<
+
+.PHONY: smtcoq_plugin.mlpack.d
+smtcoq_plugin.mlpack.d :  verit/veritParser.ml verit/veritLexer.ml smtlib2/smtlib2_parse.ml smtlib2/smtlib2_lex.ml smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml
diff --git a/src/versions/standard/Make b/src/versions/standard/_CoqProject
index e275b8f..a71f500 100644
--- a/src/versions/standard/Make
+++ b/src/versions/standard/_CoqProject
@@ -9,9 +9,6 @@
 ########################################################################
 ## To generate the Makefile:                                          ##
 ##   coq_makefile -f Make -o Makefile                                 ##
-## In the Makefile :                                                  ##
-## 1) Add "-native" to the CAMLDEP command (ocamldep -native ...)     ##
-## 2) remove "post-all" from the targets "all" and "all.timing.diff"  ##
 ########################################################################
 
 
@@ -33,20 +30,6 @@
 -I versions/standard/Int63
 -I versions/standard/Array
 
-# -I "$(shell $(COQBIN)coqc -where)/plugins/micromega"
-
--extra "test" "" "cd ../unit-tests; make"
--extra "ztest" "" "cd ../unit-tests; make zchaff"
--extra "vtest" "" "cd ../unit-tests; make verit"
--extra "lfsctest" "" "cd ../unit-tests; make lfsc"
-
--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 smtlib2/sExprParser.ml smtlib2/sExprLexer.ml lfsc/lfscParser.ml lfsc/lfscLexer.ml" ""
-
-CAMLLEX = $(CAMLBIN)ocamllex
-CAMLYACC = $(CAMLBIN)ocamlyacc
-
 versions/standard/Int63/Int63.v
 versions/standard/Int63/Int63Native.v
 versions/standard/Int63/Int63Op.v
@@ -54,6 +37,9 @@ versions/standard/Int63/Int63Axioms.v
 versions/standard/Int63/Int63Properties.v
 versions/standard/Array/PArray.v
 
+versions/standard/mutils_full.ml
+versions/standard/mutils_full.mli
+versions/standard/coq_micromega_full.ml
 versions/standard/Structures.v
 versions/standard/structures.ml
 versions/standard/structures.mli
diff --git a/src/versions/standard/coq_micromega_full.ml b/src/versions/standard/coq_micromega_full.ml
new file mode 100644
index 0000000..d957110
--- /dev/null
+++ b/src/versions/standard/coq_micromega_full.ml
@@ -0,0 +1,2215 @@
+(*** This file is taken from Coq-8.9.0 to expose more functions than
+   coq_micromega.mli does.
+   See https://github.com/coq/coq/issues/9749 . ***)
+
+
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(* ** Toplevel definition of tactics **                                 *)
+(*                                                                      *)
+(* - Modules ISet, M, Mc, Env, Cache, CacheZ                            *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2006-20011                            *)
+(*                                                                      *)
+(************************************************************************)
+
+open Pp
+open Names
+open Goptions
+open Mutils_full
+open Constr
+open Tactypes
+
+module Micromega = Micromega_plugin.Micromega
+module Certificate = Micromega_plugin.Certificate
+module Sos_types = Micromega_plugin.Sos_types
+module Mfourier = Micromega_plugin.Mfourier
+
+(**
+  * Debug flag
+  *)
+
+let debug = false
+
+(* Limit the proof search *)
+
+let max_depth = max_int
+
+(* Search limit for provers over Q R *)
+let lra_proof_depth = ref max_depth
+
+
+(* Search limit for provers over Z *)
+let lia_enum  = ref true
+let lia_proof_depth = ref max_depth
+
+let get_lia_option () =
+ (!lia_enum,!lia_proof_depth)
+
+let get_lra_option () =
+ !lra_proof_depth
+
+
+
+let _ =
+
+ let int_opt l vref =
+  {
+   optdepr = false;
+   optname = List.fold_right (^) l "";
+   optkey  = l ;
+   optread = (fun () -> Some !vref);
+   optwrite = (fun x -> vref := (match x with None -> max_depth | Some v -> v))
+  } in
+
+ let lia_enum_opt =
+  {
+   optdepr = false;
+   optname = "Lia Enum";
+   optkey  = ["Lia2";"Enum"];
+   optread = (fun () -> !lia_enum);
+   optwrite = (fun x -> lia_enum := x)
+  } in
+ let _ = declare_int_option (int_opt ["Lra2"; "Depth"] lra_proof_depth) in
+ let _ = declare_int_option (int_opt ["Lia2"; "Depth"] lia_proof_depth) in
+ let _ = declare_bool_option lia_enum_opt in
+ ()
+
+(**
+  * Initialize a tag type to the Tag module declaration (see Mutils).
+  *)
+
+type tag = Tag.t
+
+(**
+  * An atom is of the form:
+  *   pExpr1 \{<,>,=,<>,<=,>=\} pExpr2
+  * where pExpr1, pExpr2 are polynomial expressions (see Micromega). pExprs are
+  * parametrized by 'cst, which is used as the type of constants.
+  *)
+
+type 'cst atom = 'cst Micromega.formula
+
+(**
+  * Micromega's encoding of formulas.
+  * By order of appearance: boolean constants, variables, atoms, conjunctions,
+  * disjunctions, negation, implication.
+*)
+
+type 'cst formula =
+  | TT
+  | FF
+  | X of EConstr.constr
+  | A of 'cst atom * tag * EConstr.constr
+  | C of 'cst formula * 'cst formula
+  | D of 'cst formula * 'cst formula
+  | N of 'cst formula
+  | I of 'cst formula * Names.Id.t option * 'cst formula
+
+(**
+  * Formula pretty-printer.
+  *)
+
+let rec pp_formula o f =
+  match f with
+    | TT -> output_string  o "tt"
+    | FF -> output_string  o "ff"
+    | X c -> output_string o "X "
+    | A(_,t,_) -> Printf.fprintf o "A(%a)" Tag.pp t
+    | C(f1,f2) -> Printf.fprintf o "C(%a,%a)" pp_formula f1 pp_formula f2
+    | D(f1,f2) -> Printf.fprintf o "D(%a,%a)" pp_formula f1 pp_formula f2
+    | I(f1,n,f2) -> Printf.fprintf o "I(%a%s,%a)"
+	pp_formula f1
+	  (match n with
+	    | Some id -> Names.Id.to_string id
+	    | None -> "") pp_formula f2
+    | N(f) -> Printf.fprintf o "N(%a)" pp_formula f
+
+
+let rec map_atoms fct f =
+  match f with
+    | TT -> TT
+    | FF -> FF
+    | X x -> X x
+    | A (at,tg,cstr) -> A(fct at,tg,cstr)
+    | C (f1,f2) -> C(map_atoms fct f1, map_atoms fct f2)
+    | D (f1,f2) -> D(map_atoms fct f1, map_atoms fct f2)
+    | N f -> N(map_atoms fct f)
+    | I(f1,o,f2) -> I(map_atoms fct f1, o , map_atoms fct f2)
+
+let rec map_prop fct f =
+  match f with
+    | TT -> TT
+    | FF -> FF
+    | X x -> X (fct x)
+    | A (at,tg,cstr) -> A(at,tg,cstr)
+    | C (f1,f2) -> C(map_prop fct f1, map_prop fct f2)
+    | D (f1,f2) -> D(map_prop fct f1, map_prop fct f2)
+    | N f -> N(map_prop fct f)
+    | I(f1,o,f2) -> I(map_prop fct f1, o , map_prop fct f2)
+
+(**
+  * Collect the identifiers of a (string of) implications. Implication labels
+  * are inherited from Coq/CoC's higher order dependent type constructor (Pi).
+  *)
+
+let rec ids_of_formula f =
+  match f with
+    | I(f1,Some id,f2) -> id::(ids_of_formula f2)
+    | _                -> []
+
+(**
+  * A clause is a list of (tagged) nFormulas.
+  * nFormulas are normalized formulas, i.e., of the form:
+  *   cPol \{=,<>,>,>=\} 0
+  * with cPol compact polynomials (see the Pol inductive type in EnvRing.v).
+  *)
+
+type 'cst clause = ('cst Micromega.nFormula * tag) list
+
+(**
+  * A CNF is a list of clauses.
+  *)
+
+type 'cst cnf = ('cst clause) list
+
+(**
+  * True and False are empty cnfs and clauses.
+  *)
+
+let tt : 'cst cnf = []
+
+let ff : 'cst cnf = [ [] ]
+
+(**
+  * A refinement of cnf with tags left out. This is an intermediary form
+  * between the cnf tagged list representation ('cst cnf) used to solve psatz,
+  * and the freeform formulas ('cst formula) that is retrieved from Coq.
+  *)
+
+module Mc = Micromega
+
+type 'cst mc_cnf = ('cst Mc.nFormula) list list
+
+(**
+  * From a freeform formula, build a cnf.
+  * The parametric functions negate and normalize are theory-dependent, and
+  * originate in micromega.ml (extracted, e.g. for rnegate, from RMicromega.v
+  * and RingMicromega.v).
+  *)
+
+type 'a tagged_option = T of tag list |  S of 'a
+
+let cnf
+    (negate: 'cst atom -> 'cst mc_cnf) (normalise:'cst atom -> 'cst mc_cnf)
+    (unsat : 'cst Mc.nFormula -> bool) (deduce : 'cst Mc.nFormula -> 'cst Mc.nFormula -> 'cst Mc.nFormula option) (f:'cst formula) =
+
+ let negate a t =
+  List.map (fun cl -> List.map (fun x -> (x,t)) cl) (negate a) in
+
+ let normalise a t =
+  List.map (fun cl -> List.map (fun x -> (x,t)) cl) (normalise a) in
+
+ let and_cnf x y = x @ y in
+
+let rec add_term  t0 = function
+  | [] ->
+      (match deduce (fst t0) (fst t0) with
+	| Some u -> if unsat u then T [snd t0] else S (t0::[])
+	| None -> S (t0::[]))
+  | t'::cl0 ->
+      (match deduce (fst t0) (fst t') with
+	 | Some u ->
+	     if unsat u
+	     then T [snd t0 ; snd t']
+	     else (match add_term  t0 cl0 with
+		     | S cl' -> S (t'::cl')
+		     | T l -> T l)
+	 | None ->
+	     (match add_term  t0 cl0 with
+		| S cl' -> S (t'::cl')
+		| T l -> T l)) in
+
+
+ let rec or_clause  cl1 cl2 =
+   match cl1 with
+     | [] -> S cl2
+     | t0::cl ->
+	 (match add_term  t0 cl2 with
+	    | S cl' -> or_clause  cl cl'
+	    | T l -> T l) in
+
+
+
+ let or_clause_cnf t f =
+   List.fold_right (fun e (acc,tg) ->
+		      match or_clause t e with
+			| S cl -> (cl :: acc,tg)
+			| T l -> (acc,tg@l)) f ([],[]) in
+
+
+ let rec or_cnf f f' =
+  match f with
+   | [] -> tt,[]
+   | e :: rst ->
+       let (rst_f',t) = or_cnf rst f' in
+       let (e_f', t') = or_clause_cnf e f' in
+	 (rst_f' @ e_f', t @ t') in
+
+
+ let rec xcnf (polarity : bool) f =
+  match f with
+   | TT -> if polarity then (tt,[]) else (ff,[])
+   | FF  -> if polarity then (ff,[]) else (tt,[])
+   | X p -> if polarity then (ff,[]) else (ff,[])
+   | A(x,t,_) -> ((if polarity then normalise x t else negate x t),[])
+   | N(e)  -> xcnf (not polarity) e
+   | C(e1,e2) ->
+       let e1,t1 = xcnf polarity e1 in
+       let e2,t2 = xcnf polarity e2 in
+      if polarity
+       then and_cnf e1 e2, t1 @ t2
+       else let f',t' = or_cnf e1 e2 in
+	 (f', t1 @ t2 @ t')
+   | D(e1,e2)  ->
+       let e1,t1 = xcnf polarity e1 in
+       let e2,t2 = xcnf polarity e2 in
+      if polarity
+       then let f',t' = or_cnf e1 e2 in
+	 (f', t1 @ t2 @ t')
+       else and_cnf e1 e2, t1 @ t2
+   | I(e1,_,e2) ->
+       let e1 , t1 = (xcnf (not polarity) e1) in
+       let e2 , t2 = (xcnf polarity e2) in
+      if polarity
+       then let f',t' = or_cnf e1 e2 in
+	 (f', t1 @ t2 @ t')
+       else and_cnf e1 e2, t1 @ t2 in
+
+  xcnf true f
+
+(**
+  * MODULE: Ordered set of integers.
+  *)
+
+module ISet = Set.Make(Int)
+
+(**
+  * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of
+  * elements of m that are at position i0,...,iN.
+  *)
+
+let selecti s m =
+  let rec xselecti i m =
+    match m with
+      | [] -> []
+      | e::m -> if ISet.mem i s then e::(xselecti (i+1) m) else xselecti (i+1) m in
+    xselecti 0 m
+
+(**
+  * MODULE: Mapping of the Coq data-strustures into Caml and Caml extracted
+  * code. This includes initializing Caml variables based on Coq terms, parsing
+  * various Coq expressions into Caml, and dumping Caml expressions into Coq.
+  *
+  * Opened here and in csdpcert.ml.
+  *)
+
+module M =
+struct
+
+  (**
+    * Location of the Coq libraries.
+    *)
+
+  let logic_dir = ["Coq";"Logic";"Decidable"]
+
+  let mic_modules =
+    [
+      ["Coq";"Lists";"List"];
+      ["ZMicromega"];
+      ["Tauto"];
+      ["RingMicromega"];
+      ["EnvRing"];
+      ["Coq"; "micromega"; "ZMicromega"];
+      ["Coq"; "micromega"; "RMicromega"];
+      ["Coq" ; "micromega" ; "Tauto"];
+      ["Coq" ; "micromega" ; "RingMicromega"];
+      ["Coq" ; "micromega" ; "EnvRing"];
+      ["Coq";"QArith"; "QArith_base"];
+      ["Coq";"Reals" ; "Rdefinitions"];
+      ["Coq";"Reals" ; "Rpow_def"];
+      ["LRing_normalise"]]
+
+  let coq_modules =
+   Coqlib.(init_modules @
+    [logic_dir] @ arith_modules @ zarith_base_modules @ mic_modules)
+
+  let bin_module = [["Coq";"Numbers";"BinNums"]]
+
+  let r_modules =
+    [["Coq";"Reals" ; "Rdefinitions"];
+     ["Coq";"Reals" ; "Rpow_def"] ;
+     ["Coq";"Reals" ; "Raxioms"] ;
+     ["Coq";"QArith"; "Qreals"] ;
+    ]
+
+  let z_modules = [["Coq";"ZArith";"BinInt"]]
+
+  (**
+    * Initialization : a large amount of Caml symbols are derived from
+    * ZMicromega.v
+    *)
+
+  let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n)
+  let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules
+  let constant = gen_constant_in_modules "ZMicromega" coq_modules
+  let bin_constant = gen_constant_in_modules "ZMicromega" bin_module
+  let r_constant = gen_constant_in_modules "ZMicromega" r_modules
+  let z_constant = gen_constant_in_modules "ZMicromega" z_modules
+  let m_constant = gen_constant_in_modules "ZMicromega" mic_modules
+
+  let coq_and = lazy (init_constant "and")
+  let coq_or = lazy (init_constant "or")
+  let coq_not = lazy (init_constant "not")
+
+  let coq_iff = lazy (init_constant "iff")
+  let coq_True = lazy (init_constant "True")
+  let coq_False = lazy (init_constant "False")
+
+  let coq_cons = lazy (constant "cons")
+  let coq_nil = lazy (constant "nil")
+  let coq_list = lazy (constant "list")
+
+  let coq_O = lazy (init_constant "O")
+  let coq_S = lazy (init_constant "S")
+
+  let coq_N0 = lazy (bin_constant "N0")
+  let coq_Npos = lazy (bin_constant "Npos")
+
+  let coq_xH = lazy (bin_constant "xH")
+  let coq_xO = lazy (bin_constant "xO")
+  let coq_xI = lazy (bin_constant "xI")
+
+  let coq_Z = lazy (bin_constant "Z")
+  let coq_ZERO = lazy (bin_constant "Z0")
+  let coq_POS = lazy (bin_constant "Zpos")
+  let coq_NEG = lazy (bin_constant "Zneg")
+
+  let coq_Q = lazy (constant "Q")
+  let coq_R = lazy (constant "R")
+
+  let coq_Qmake = lazy (constant "Qmake")
+
+  let coq_Rcst = lazy (constant "Rcst")
+
+  let coq_C0   = lazy (m_constant "C0")
+  let coq_C1   = lazy (m_constant "C1")
+  let coq_CQ   = lazy (m_constant "CQ")
+  let coq_CZ   = lazy (m_constant "CZ")
+  let coq_CPlus = lazy (m_constant "CPlus")
+  let coq_CMinus = lazy (m_constant "CMinus")
+  let coq_CMult  = lazy (m_constant "CMult")
+  let coq_CInv   = lazy (m_constant "CInv")
+  let coq_COpp   = lazy (m_constant "COpp")
+
+
+  let coq_R0    = lazy (constant "R0")
+  let coq_R1    = lazy (constant "R1")
+
+  let coq_proofTerm = lazy (constant "ZArithProof")
+  let coq_doneProof = lazy (constant "DoneProof")
+  let coq_ratProof = lazy (constant "RatProof")
+  let coq_cutProof = lazy (constant "CutProof")
+  let coq_enumProof = lazy (constant "EnumProof")
+
+  let coq_Zgt = lazy (z_constant "Z.gt")
+  let coq_Zge = lazy (z_constant "Z.ge")
+  let coq_Zle = lazy (z_constant "Z.le")
+  let coq_Zlt = lazy (z_constant "Z.lt")
+  let coq_Eq  = lazy (init_constant "eq")
+
+  let coq_Zplus = lazy (z_constant "Z.add")
+  let coq_Zminus = lazy (z_constant "Z.sub")
+  let coq_Zopp = lazy (z_constant "Z.opp")
+  let coq_Zmult = lazy (z_constant "Z.mul")
+  let coq_Zpower = lazy (z_constant "Z.pow")
+
+  let coq_Qle = lazy (constant "Qle")
+  let coq_Qlt = lazy (constant "Qlt")
+  let coq_Qeq = lazy (constant "Qeq")
+
+  let coq_Qplus = lazy (constant "Qplus")
+  let coq_Qminus = lazy (constant "Qminus")
+  let coq_Qopp = lazy (constant "Qopp")
+  let coq_Qmult = lazy (constant "Qmult")
+  let coq_Qpower = lazy (constant "Qpower")
+
+  let coq_Rgt = lazy (r_constant "Rgt")
+  let coq_Rge = lazy (r_constant "Rge")
+  let coq_Rle = lazy (r_constant "Rle")
+  let coq_Rlt = lazy (r_constant "Rlt")
+
+  let coq_Rplus = lazy (r_constant "Rplus")
+  let coq_Rminus = lazy (r_constant "Rminus")
+  let coq_Ropp = lazy (r_constant "Ropp")
+  let coq_Rmult = lazy (r_constant "Rmult")
+  let coq_Rinv = lazy (r_constant "Rinv")
+  let coq_Rpower = lazy (r_constant "pow")
+  let coq_IZR    = lazy (r_constant "IZR")
+  let coq_IQR    = lazy (r_constant "Q2R")
+
+
+  let coq_PEX = lazy (constant "PEX" )
+  let coq_PEc = lazy (constant"PEc")
+  let coq_PEadd = lazy (constant "PEadd")
+  let coq_PEopp = lazy (constant "PEopp")
+  let coq_PEmul = lazy (constant "PEmul")
+  let coq_PEsub = lazy (constant "PEsub")
+  let coq_PEpow = lazy (constant "PEpow")
+
+  let coq_PX = lazy (constant "PX" )
+  let coq_Pc = lazy (constant"Pc")
+  let coq_Pinj = lazy (constant "Pinj")
+
+  let coq_OpEq = lazy (constant "OpEq")
+  let coq_OpNEq = lazy (constant "OpNEq")
+  let coq_OpLe = lazy (constant "OpLe")
+  let coq_OpLt = lazy (constant  "OpLt")
+  let coq_OpGe = lazy (constant "OpGe")
+  let coq_OpGt = lazy (constant  "OpGt")
+
+  let coq_PsatzIn = lazy (constant "PsatzIn")
+  let coq_PsatzSquare = lazy (constant "PsatzSquare")
+  let coq_PsatzMulE = lazy (constant "PsatzMulE")
+  let coq_PsatzMultC = lazy (constant "PsatzMulC")
+  let coq_PsatzAdd  = lazy (constant "PsatzAdd")
+  let coq_PsatzC  = lazy (constant "PsatzC")
+  let coq_PsatzZ    = lazy (constant "PsatzZ")
+
+  let coq_TT = lazy
+   (gen_constant_in_modules "ZMicromega"
+     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "TT")
+  let coq_FF = lazy
+   (gen_constant_in_modules "ZMicromega"
+     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "FF")
+  let coq_And = lazy
+   (gen_constant_in_modules "ZMicromega"
+     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "Cj")
+  let coq_Or = lazy
+   (gen_constant_in_modules "ZMicromega"
+     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]    "D")
+  let coq_Neg = lazy
+   (gen_constant_in_modules "ZMicromega"
+     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "N")
+  let coq_Atom = lazy
+   (gen_constant_in_modules "ZMicromega"
+     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "A")
+  let coq_X = lazy
+   (gen_constant_in_modules "ZMicromega"
+     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "X")
+  let coq_Impl = lazy
+   (gen_constant_in_modules "ZMicromega"
+     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "I")
+  let coq_Formula = lazy
+   (gen_constant_in_modules "ZMicromega"
+     [["Coq" ; "micromega" ; "Tauto"];["Tauto"]]  "BFormula")
+
+  (**
+    * Initialization : a few Caml symbols are derived from other libraries;
+    * QMicromega, ZArithRing, RingMicromega.
+    *)
+
+  let coq_QWitness = lazy
+   (gen_constant_in_modules "QMicromega"
+     [["Coq"; "micromega"; "QMicromega"]] "QWitness")
+
+  let coq_Build = lazy
+   (gen_constant_in_modules "RingMicromega"
+     [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ]
+     "Build_Formula")
+  let coq_Cstr = lazy
+   (gen_constant_in_modules "RingMicromega"
+     [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] "Formula")
+
+  (**
+    * Parsing and dumping : transformation functions between Caml and Coq
+    * data-structures.
+    *
+    * dump_*    functions go from Micromega to Coq terms
+    * parse_*   functions go from Coq to Micromega terms
+    * pp_*      functions pretty-print Coq terms.
+    *)
+
+  exception ParseError
+
+  (* A simple but useful getter function *)
+
+  let get_left_construct sigma term =
+   match EConstr.kind sigma term with
+    | Construct((_,i),_) -> (i,[| |])
+    | App(l,rst) ->
+       (match EConstr.kind sigma l with
+        | Construct((_,i),_) -> (i,rst)
+        |   _     -> raise ParseError
+       )
+    | _ ->   raise ParseError
+
+  (* Access the Micromega module *)
+
+  (* parse/dump/print from numbers up to expressions and formulas *)
+
+  let rec parse_nat sigma term =
+   let (i,c) = get_left_construct sigma term in
+    match i with
+     | 1 -> Mc.O
+     | 2 -> Mc.S (parse_nat sigma (c.(0)))
+     | i -> raise ParseError
+
+  let pp_nat o n = Printf.fprintf o "%i" (CoqToCaml.nat n)
+
+  let rec dump_nat x =
+   match x with
+    | Mc.O -> Lazy.force coq_O
+    | Mc.S p -> EConstr.mkApp(Lazy.force coq_S,[| dump_nat p |])
+
+  let rec parse_positive sigma term =
+   let (i,c) = get_left_construct sigma term in
+    match i with
+     | 1 -> Mc.XI (parse_positive sigma c.(0))
+     | 2 -> Mc.XO (parse_positive sigma c.(0))
+     | 3 -> Mc.XH
+     | i -> raise ParseError
+
+  let rec dump_positive x =
+   match x with
+    | Mc.XH -> Lazy.force coq_xH
+    | Mc.XO p -> EConstr.mkApp(Lazy.force coq_xO,[| dump_positive p |])
+    | Mc.XI p -> EConstr.mkApp(Lazy.force coq_xI,[| dump_positive p |])
+
+  let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x)
+
+  let dump_n x =
+   match x with
+    | Mc.N0 -> Lazy.force coq_N0
+    | Mc.Npos p -> EConstr.mkApp(Lazy.force coq_Npos,[| dump_positive p|])
+
+  let parse_z sigma term =
+   let (i,c) = get_left_construct sigma term in
+    match i with
+     | 1 -> Mc.Z0
+     | 2 -> Mc.Zpos (parse_positive sigma c.(0))
+     | 3 -> Mc.Zneg (parse_positive sigma c.(0))
+     | i -> raise ParseError
+
+  let dump_z x =
+   match x with
+    | Mc.Z0 ->Lazy.force coq_ZERO
+    | Mc.Zpos p -> EConstr.mkApp(Lazy.force coq_POS,[| dump_positive p|])
+    | Mc.Zneg p -> EConstr.mkApp(Lazy.force coq_NEG,[| dump_positive p|])
+
+  let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (CoqToCaml.z_big_int x))
+
+  let dump_q q =
+   EConstr.mkApp(Lazy.force coq_Qmake,
+                 [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|])
+
+  let parse_q sigma term =
+     match EConstr.kind sigma term with
+       | App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then
+             {Mc.qnum = parse_z sigma args.(0) ; Mc.qden = parse_positive sigma args.(1) }
+       else raise ParseError
+   |  _ -> raise ParseError
+
+
+  let rec pp_Rcst o cst =
+    match cst with
+      | Mc.C0 -> output_string o "C0"
+      | Mc.C1 ->  output_string o "C1"
+      | Mc.CQ q ->  output_string o "CQ _"
+      | Mc.CZ z -> pp_z o z
+      | Mc.CPlus(x,y) -> Printf.fprintf o "(%a + %a)" pp_Rcst x pp_Rcst y
+      | Mc.CMinus(x,y) -> Printf.fprintf o "(%a - %a)" pp_Rcst x pp_Rcst y
+      | Mc.CMult(x,y) -> Printf.fprintf o "(%a * %a)" pp_Rcst x pp_Rcst y
+      | Mc.CInv t -> Printf.fprintf o "(/ %a)" pp_Rcst t
+      | Mc.COpp t -> Printf.fprintf o "(- %a)" pp_Rcst t
+
+
+  let rec dump_Rcst cst =
+    match cst with
+      | Mc.C0 -> Lazy.force coq_C0
+      | Mc.C1 ->  Lazy.force coq_C1
+      | Mc.CQ q ->  EConstr.mkApp(Lazy.force coq_CQ, [| dump_q q |])
+      | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_CZ, [| dump_z z |])
+      | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_CPlus, [| dump_Rcst x ; dump_Rcst y |])
+      | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_CMinus, [| dump_Rcst x ; dump_Rcst y |])
+      | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_CMult, [| dump_Rcst x ; dump_Rcst y |])
+      | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_CInv, [| dump_Rcst t |])
+      | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_COpp, [| dump_Rcst t |])
+
+  let rec dump_list typ dump_elt l =
+   match l with
+    | [] -> EConstr.mkApp(Lazy.force coq_nil,[| typ |])
+    | e :: l -> EConstr.mkApp(Lazy.force coq_cons,
+                                [| typ; dump_elt e;dump_list typ dump_elt l|])
+
+  let pp_list op cl elt o l =
+   let rec _pp  o l =
+    match l with
+     | [] -> ()
+     | [e] -> Printf.fprintf o "%a" elt e
+     | e::l -> Printf.fprintf o "%a ,%a" elt e  _pp l in
+    Printf.fprintf o "%s%a%s" op _pp l cl
+
+  let dump_var = dump_positive
+
+  let dump_expr typ dump_z e =
+   let rec dump_expr  e =
+   match e with
+    | Mc.PEX n -> EConstr.mkApp(Lazy.force coq_PEX,[| typ; dump_var n |])
+    | Mc.PEc z -> EConstr.mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |])
+    | Mc.PEadd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEadd,
+                                       [| typ; dump_expr e1;dump_expr e2|])
+    | Mc.PEsub(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEsub,
+                                       [| typ; dump_expr  e1;dump_expr  e2|])
+    | Mc.PEopp e -> EConstr.mkApp(Lazy.force coq_PEopp,
+                                  [| typ; dump_expr  e|])
+    | Mc.PEmul(e1,e2) ->  EConstr.mkApp(Lazy.force coq_PEmul,
+                                        [| typ; dump_expr  e1;dump_expr e2|])
+    | Mc.PEpow(e,n) ->  EConstr.mkApp(Lazy.force coq_PEpow,
+                                      [| typ; dump_expr  e; dump_n  n|])
+      in
+    dump_expr e
+
+  let dump_pol typ dump_c e =
+    let rec dump_pol e =
+      match e with
+        | Mc.Pc n -> EConstr.mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|])
+        | Mc.Pinj(p,pol) -> EConstr.mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|])
+        | Mc.PX(pol1,p,pol2) -> EConstr.mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in
+      dump_pol e
+
+  let pp_pol pp_c o e =
+    let rec pp_pol o e =
+      match e with
+        | Mc.Pc n -> Printf.fprintf o "Pc %a" pp_c n
+        | Mc.Pinj(p,pol) -> Printf.fprintf o "Pinj(%a,%a)" pp_positive p pp_pol pol
+        | Mc.PX(pol1,p,pol2) -> Printf.fprintf o "PX(%a,%a,%a)" pp_pol pol1 pp_positive p pp_pol pol2 in
+      pp_pol o e
+
+  let pp_cnf pp_c o f =
+    let pp_clause o l = List.iter (fun ((p,_),t) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c)  p Tag.pp t) l in
+      List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause l) f
+
+  let dump_psatz typ dump_z e =
+   let z = Lazy.force typ in
+  let rec dump_cone e =
+   match e with
+    | Mc.PsatzIn n -> EConstr.mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |])
+    | Mc.PsatzMulC(e,c) -> EConstr.mkApp(Lazy.force coq_PsatzMultC,
+                                         [| z; dump_pol z dump_z e ; dump_cone c |])
+    | Mc.PsatzSquare e -> EConstr.mkApp(Lazy.force coq_PsatzSquare,
+                                        [| z;dump_pol z dump_z e|])
+    | Mc.PsatzAdd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzAdd,
+                                          [| z; dump_cone e1; dump_cone e2|])
+    | Mc.PsatzMulE(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzMulE,
+                                           [| z; dump_cone e1; dump_cone e2|])
+    | Mc.PsatzC p -> EConstr.mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|])
+    | Mc.PsatzZ    -> EConstr.mkApp(Lazy.force coq_PsatzZ,[| z|]) in
+   dump_cone e
+
+  let  pp_psatz pp_z o e =
+   let rec pp_cone o e =
+    match e with
+     | Mc.PsatzIn n ->
+        Printf.fprintf o "(In %a)%%nat" pp_nat n
+     | Mc.PsatzMulC(e,c) ->
+        Printf.fprintf o "( %a [*] %a)" (pp_pol pp_z) e pp_cone c
+     | Mc.PsatzSquare e ->
+        Printf.fprintf o "(%a^2)" (pp_pol pp_z) e
+     | Mc.PsatzAdd(e1,e2) ->
+        Printf.fprintf o "(%a [+] %a)" pp_cone e1 pp_cone e2
+     | Mc.PsatzMulE(e1,e2) ->
+        Printf.fprintf o "(%a [*] %a)" pp_cone e1 pp_cone e2
+     | Mc.PsatzC p ->
+        Printf.fprintf o "(%a)%%positive" pp_z p
+     | Mc.PsatzZ    ->
+        Printf.fprintf o "0" in
+    pp_cone o e
+
+  let dump_op = function
+   | Mc.OpEq-> Lazy.force coq_OpEq
+   | Mc.OpNEq-> Lazy.force coq_OpNEq
+   | Mc.OpLe -> Lazy.force coq_OpLe
+   | Mc.OpGe -> Lazy.force coq_OpGe
+   | Mc.OpGt-> Lazy.force coq_OpGt
+   | Mc.OpLt-> Lazy.force coq_OpLt
+
+  let dump_cstr typ dump_constant {Mc.flhs = e1 ; Mc.fop = o ; Mc.frhs = e2} =
+    EConstr.mkApp(Lazy.force coq_Build,
+                  [| typ; dump_expr typ dump_constant e1 ;
+                     dump_op o ;
+                     dump_expr typ dump_constant e2|])
+
+  let assoc_const sigma x l =
+   try
+   snd (List.find (fun (x',y) -> EConstr.eq_constr sigma x (Lazy.force x')) l)
+   with
+     Not_found -> raise ParseError
+
+  let zop_table = [
+   coq_Zgt, Mc.OpGt ;
+   coq_Zge, Mc.OpGe ;
+   coq_Zlt, Mc.OpLt ;
+   coq_Zle, Mc.OpLe ]
+
+  let rop_table = [
+   coq_Rgt, Mc.OpGt ;
+   coq_Rge, Mc.OpGe ;
+   coq_Rlt, Mc.OpLt ;
+   coq_Rle, Mc.OpLe ]
+
+  let qop_table = [
+   coq_Qlt, Mc.OpLt ;
+   coq_Qle, Mc.OpLe ;
+   coq_Qeq, Mc.OpEq
+  ]
+
+  type gl = { env : Environ.env; sigma : Evd.evar_map }
+
+  let is_convertible gl t1 t2 =
+   Reductionops.is_conv gl.env gl.sigma t1 t2
+
+  let parse_zop gl (op,args) =
+    let sigma = gl.sigma in
+    match EConstr.kind sigma op with
+    | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1))
+    | Ind((n,0),_) ->
+        if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z)
+        then (Mc.OpEq, args.(1), args.(2))
+        else raise ParseError
+    |   _ -> failwith "parse_zop"
+
+  let parse_rop gl (op,args) =
+    let sigma = gl.sigma in
+    match EConstr.kind sigma op with
+     | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1))
+     | Ind((n,0),_) ->
+        if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R)
+        then (Mc.OpEq, args.(1), args.(2))
+        else raise ParseError
+    |   _ -> failwith "parse_zop"
+
+  let parse_qop gl (op,args) =
+    (assoc_const gl.sigma op qop_table, args.(0) , args.(1))
+
+  type 'a op =
+    | Binop of ('a Mc.pExpr -> 'a Mc.pExpr -> 'a Mc.pExpr)
+    | Opp
+    | Power
+    | Ukn of string
+
+  let assoc_ops sigma x l =
+   try
+     snd (List.find (fun (x',y) -> EConstr.eq_constr sigma x (Lazy.force x')) l)
+   with
+     Not_found -> Ukn "Oups"
+
+  (**
+    * MODULE: Env is for environment.
+    *)
+
+  module Env =
+  struct
+   let compute_rank_add env sigma v =
+    let rec _add env n v =
+     match env with
+      | [] -> ([v],n)
+      | e::l ->
+         if EConstr.eq_constr sigma e v
+         then (env,n)
+         else
+          let (env,n) = _add l ( n+1) v in
+           (e::env,n) in
+    let (env, n) =  _add env 1 v in
+     (env, CamlToCoq.positive n)
+
+   let get_rank env sigma v =
+
+     let rec _get_rank env n =
+       match env with
+       | [] -> raise (Invalid_argument "get_rank")
+      | e::l ->
+         if EConstr.eq_constr sigma e v
+         then n
+         else  _get_rank l (n+1)  in
+     _get_rank env 1
+
+
+   let empty = []
+
+   let elements env = env
+
+  end (* MODULE END: Env *)
+
+  (**
+    * This is the big generic function for expression parsers.
+    *)
+
+  let parse_expr sigma parse_constant parse_exp ops_spec env term =
+    if debug
+    then (
+      let _, env = Pfedit.get_current_context () in
+      Feedback.msg_debug (Pp.str "parse_expr: " ++ Printer.pr_leconstr_env env sigma term));
+
+(*
+    let constant_or_variable env term =
+     try
+      ( Mc.PEc (parse_constant term) , env)
+     with ParseError ->
+      let (env,n) = Env.compute_rank_add env term in
+       (Mc.PEX  n , env) in
+*)
+    let parse_variable env term =
+      let (env,n) = Env.compute_rank_add env sigma term in
+	(Mc.PEX  n , env) in
+
+    let rec parse_expr env term =
+     let combine env op (t1,t2) =
+      let (expr1,env) = parse_expr env t1 in
+      let (expr2,env) = parse_expr env t2 in
+      (op expr1 expr2,env) in
+
+       try (Mc.PEc (parse_constant term) , env)
+       with ParseError ->
+	 match EConstr.kind sigma term with
+           | App(t,args) ->
+               (
+		 match EConstr.kind sigma t with
+                   | Const c ->
+		       ( match assoc_ops sigma t ops_spec  with
+			   | Binop f -> combine env f (args.(0),args.(1))
+                   | Opp     -> let (expr,env) = parse_expr env args.(0) in
+                       (Mc.PEopp expr, env)
+                   | Power   ->
+                       begin
+			 try
+                           let (expr,env) = parse_expr env args.(0) in
+                           let power = (parse_exp expr args.(1)) in
+                             (power  , env)
+			 with e when CErrors.noncritical e ->
+                           (* if the exponent is a variable *)
+                           let (env,n) = Env.compute_rank_add env sigma term in (Mc.PEX n, env)
+                       end
+                   | Ukn  s ->
+                       if debug
+                       then (Printf.printf "unknown op: %s\n" s; flush stdout;);
+                       let (env,n) = Env.compute_rank_add env sigma term in (Mc.PEX n, env)
+               )
+		   |   _ -> parse_variable env term
+               )
+	   | _ -> parse_variable env term in
+     parse_expr env term
+
+  let zop_spec =
+    [
+      coq_Zplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+      coq_Zminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+      coq_Zmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ;
+      coq_Zopp   , Opp ;
+      coq_Zpower , Power]
+
+  let qop_spec =
+   [
+      coq_Qplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+      coq_Qminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+      coq_Qmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ;
+      coq_Qopp   , Opp ;
+      coq_Qpower , Power]
+
+  let rop_spec =
+   [
+      coq_Rplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+      coq_Rminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+      coq_Rmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ;
+      coq_Ropp   , Opp ;
+      coq_Rpower , Power]
+
+  let zconstant = parse_z
+  let qconstant = parse_q
+
+
+  let rconst_assoc =
+    [
+      coq_Rplus , (fun x y -> Mc.CPlus(x,y)) ;
+      coq_Rminus , (fun x y -> Mc.CMinus(x,y)) ;
+      coq_Rmult  , (fun x y -> Mc.CMult(x,y)) ;
+    (*      coq_Rdiv   , (fun x y -> Mc.CMult(x,Mc.CInv y)) ;*)
+    ]
+
+  let rec rconstant sigma term =
+   match EConstr.kind sigma term with
+    | Const x ->
+        if EConstr.eq_constr sigma term (Lazy.force coq_R0)
+        then Mc.C0
+        else if EConstr.eq_constr sigma term (Lazy.force coq_R1)
+        then Mc.C1
+        else raise ParseError
+    | App(op,args) ->
+	begin
+	  try
+            (* the evaluation order is important in the following *)
+            let f = assoc_const sigma op rconst_assoc in
+            let a = rconstant sigma args.(0) in
+            let b = rconstant sigma args.(1) in
+            f a b
+	  with
+	      ParseError ->
+		match op with
+		| op when EConstr.eq_constr sigma op (Lazy.force coq_Rinv) ->
+                  let arg = rconstant sigma args.(0) in
+                  if Mc.qeq_bool (Mc.q_of_Rcst arg) {Mc.qnum = Mc.Z0 ; Mc.qden = Mc.XH}
+                  then raise ParseError (* This is a division by zero -- no semantics *)
+                  else Mc.CInv(arg)
+		| op when EConstr.eq_constr sigma op (Lazy.force coq_IQR)  -> Mc.CQ (parse_q sigma args.(0))
+		| op when EConstr.eq_constr sigma op   (Lazy.force coq_IZR)  -> Mc.CZ (parse_z sigma args.(0))
+		| _ ->  raise ParseError
+	end
+
+    |  _ -> raise ParseError
+
+
+  let rconstant sigma term =
+    let _, env = Pfedit.get_current_context () in
+    if debug
+    then Feedback.msg_debug (Pp.str "rconstant: " ++ Printer.pr_leconstr_env env sigma term ++ fnl ());
+    let res = rconstant sigma term in
+      if debug then
+	(Printf.printf "rconstant -> %a\n" pp_Rcst res ; flush stdout) ;
+      res
+
+
+  let parse_zexpr sigma =  parse_expr sigma
+    (zconstant sigma)
+    (fun expr x ->
+      let exp = (parse_z sigma x) in
+        match exp with
+          | Mc.Zneg _ -> Mc.PEc Mc.Z0
+          |   _     ->  Mc.PEpow(expr, Mc.Z.to_N exp))
+    zop_spec
+
+  let parse_qexpr sigma =  parse_expr sigma
+   (qconstant sigma)
+    (fun expr x ->
+      let exp = parse_z sigma x in
+        match exp with
+          | Mc.Zneg _ ->
+              begin
+                match expr with
+                | Mc.PEc q -> Mc.PEc (Mc.qpower q exp)
+                |     _    -> print_string "parse_qexpr parse error" ; flush stdout ; raise ParseError
+              end
+          | _     ->  let exp = Mc.Z.to_N  exp in
+                        Mc.PEpow(expr,exp))
+   qop_spec
+
+  let parse_rexpr sigma =  parse_expr sigma
+   (rconstant sigma)
+   (fun expr x ->
+      let exp = Mc.N.of_nat (parse_nat sigma x) in
+        Mc.PEpow(expr,exp))
+   rop_spec
+
+  let  parse_arith parse_op parse_expr env cstr gl =
+    let sigma = gl.sigma in
+    if debug
+    then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr_env gl.env sigma cstr ++ fnl ());
+    match EConstr.kind sigma cstr with
+    | App(op,args) ->
+       let (op,lhs,rhs) = parse_op gl (op,args) in
+       let (e1,env) = parse_expr sigma env lhs in
+       let (e2,env) = parse_expr sigma env rhs in
+        ({Mc.flhs = e1; Mc.fop = op;Mc.frhs = e2},env)
+    |  _ -> failwith "error : parse_arith(2)"
+
+  let parse_zarith = parse_arith parse_zop parse_zexpr
+
+  let parse_qarith = parse_arith parse_qop parse_qexpr
+
+  let parse_rarith = parse_arith parse_rop parse_rexpr
+
+  (* generic parsing of arithmetic expressions *)
+
+  let mkC f1 f2 = C(f1,f2)
+  let mkD f1 f2 = D(f1,f2)
+  let mkIff f1 f2 = C(I(f1,None,f2),I(f2,None,f1))
+  let mkI f1 f2 = I(f1,None,f2)
+
+  let mkformula_binary g term f1 f2 =
+    match f1 , f2 with
+    |  X _  , X _ -> X(term)
+    |   _         -> g f1 f2
+
+  (**
+    * This is the big generic function for formula parsers.
+    *)
+
+  let parse_formula gl parse_atom env tg term =
+    let sigma = gl.sigma in
+
+    let parse_atom env tg t =
+      try
+        let (at,env) = parse_atom env t gl in
+        (A(at,tg,t), env,Tag.next tg)
+      with e when CErrors.noncritical e -> (X(t),env,tg) in
+
+    let is_prop term =
+      let sort  = Retyping.get_sort_of gl.env gl.sigma term in
+     Sorts.is_prop sort in
+
+    let rec xparse_formula env tg term =
+      match EConstr.kind sigma term with
+      | App(l,rst) ->
+        (match rst with
+        | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_and) ->
+          let f,env,tg = xparse_formula env tg a in
+          let g,env, tg = xparse_formula env tg b  in
+          mkformula_binary mkC term f g,env,tg
+        | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_or) ->
+          let f,env,tg = xparse_formula env tg a in
+          let g,env,tg  = xparse_formula env tg b in
+          mkformula_binary mkD term f g,env,tg
+        | [|a|] when EConstr.eq_constr sigma l (Lazy.force coq_not) ->
+          let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg)
+        | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_iff) ->
+          let f,env,tg = xparse_formula env tg a in
+          let g,env,tg = xparse_formula env tg b in
+          mkformula_binary mkIff term f g,env,tg
+        | _ -> parse_atom env tg term)
+      | Prod(typ,a,b) when EConstr.Vars.noccurn sigma 1 b ->
+        let f,env,tg = xparse_formula env tg a in
+        let g,env,tg = xparse_formula env tg b in
+        mkformula_binary mkI term f g,env,tg
+      | _ when EConstr.eq_constr sigma term (Lazy.force coq_True) -> (TT,env,tg)
+      | _ when EConstr.eq_constr sigma term (Lazy.force coq_False) -> (FF,env,tg)
+      | _ when is_prop term -> X(term),env,tg
+      | _ -> raise ParseError
+    in
+    xparse_formula env tg  ((*Reductionops.whd_zeta*) term)
+
+  let dump_formula typ dump_atom f =
+   let rec xdump f =
+    match f with
+     | TT  -> EConstr.mkApp(Lazy.force coq_TT,[|typ|])
+     | FF  -> EConstr.mkApp(Lazy.force coq_FF,[|typ|])
+     | C(x,y) -> EConstr.mkApp(Lazy.force coq_And,[|typ ; xdump x ; xdump y|])
+     | D(x,y) -> EConstr.mkApp(Lazy.force coq_Or,[|typ ; xdump x ; xdump y|])
+     | I(x,_,y) -> EConstr.mkApp(Lazy.force coq_Impl,[|typ ; xdump x ; xdump y|])
+     | N(x) -> EConstr.mkApp(Lazy.force coq_Neg,[|typ ; xdump x|])
+     | A(x,_,_) -> EConstr.mkApp(Lazy.force coq_Atom,[|typ ; dump_atom x|])
+     | X(t) -> EConstr.mkApp(Lazy.force coq_X,[|typ ; t|])  in
+   xdump f
+
+
+  let prop_env_of_formula sigma form =
+    let rec doit env = function
+      | TT | FF | A(_,_,_) -> env
+      | X t -> fst (Env.compute_rank_add env sigma t)
+      | C(f1,f2) | D(f1,f2) | I(f1,_,f2) ->
+        doit (doit env f1) f2
+      | N f -> doit env f in
+
+    doit [] form
+
+  let var_env_of_formula form =
+
+    let rec vars_of_expr  = function
+      | Mc.PEX n -> ISet.singleton (CoqToCaml.positive n)
+      | Mc.PEc z -> ISet.empty
+      | Mc.PEadd(e1,e2) | Mc.PEmul(e1,e2) | Mc.PEsub(e1,e2) ->
+        ISet.union (vars_of_expr e1) (vars_of_expr e2)
+      | Mc.PEopp e | Mc.PEpow(e,_)-> vars_of_expr e
+    in
+
+    let vars_of_atom  {Mc.flhs ; Mc.fop; Mc.frhs} =
+      ISet.union (vars_of_expr flhs) (vars_of_expr frhs) in
+
+    let rec doit = function
+      |  TT | FF | X _ -> ISet.empty
+      | A (a,t,c) -> vars_of_atom a
+      | C(f1,f2) | D(f1,f2) |I (f1,_,f2) -> ISet.union (doit f1) (doit f2)
+      | N f -> doit f in
+
+    doit  form
+
+
+
+
+  type 'cst dump_expr =  (* 'cst is the type of the syntactic constants *)
+    {
+      interp_typ : EConstr.constr;
+      dump_cst : 'cst -> EConstr.constr;
+      dump_add : EConstr.constr;
+      dump_sub : EConstr.constr;
+      dump_opp : EConstr.constr;
+      dump_mul : EConstr.constr;
+      dump_pow : EConstr.constr;
+      dump_pow_arg : Mc.n -> EConstr.constr;
+      dump_op  : (Mc.op2 * EConstr.constr) list
+    }
+
+let dump_zexpr = lazy
+  {
+    interp_typ = Lazy.force coq_Z;
+    dump_cst = dump_z;
+    dump_add = Lazy.force coq_Zplus;
+    dump_sub = Lazy.force coq_Zminus;
+    dump_opp = Lazy.force coq_Zopp;
+    dump_mul = Lazy.force coq_Zmult;
+    dump_pow = Lazy.force coq_Zpower;
+    dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)));
+    dump_op  = List.map (fun (x,y) -> (y,Lazy.force x)) zop_table
+  }
+
+let dump_qexpr = lazy
+  {
+    interp_typ = Lazy.force coq_Q;
+    dump_cst = dump_q;
+    dump_add = Lazy.force coq_Qplus;
+    dump_sub = Lazy.force coq_Qminus;
+    dump_opp = Lazy.force coq_Qopp;
+    dump_mul = Lazy.force coq_Qmult;
+    dump_pow = Lazy.force coq_Qpower;
+    dump_pow_arg = (fun n -> dump_z (CamlToCoq.z (CoqToCaml.n n)));
+    dump_op  = List.map (fun (x,y) -> (y,Lazy.force x)) qop_table
+  }
+
+let rec dump_Rcst_as_R cst =
+  match cst with
+  | Mc.C0 -> Lazy.force coq_R0
+  | Mc.C1 ->  Lazy.force coq_R1
+  | Mc.CQ q ->  EConstr.mkApp(Lazy.force coq_IQR, [| dump_q q |])
+  | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_IZR, [| dump_z z |])
+  | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_Rplus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+  | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_Rminus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+  | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_Rmult, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |])
+  | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_Rinv, [| dump_Rcst_as_R t |])
+  | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_Ropp, [| dump_Rcst_as_R t |])
+
+
+let dump_rexpr = lazy
+  {
+    interp_typ = Lazy.force coq_R;
+    dump_cst = dump_Rcst_as_R;
+    dump_add = Lazy.force coq_Rplus;
+    dump_sub = Lazy.force coq_Rminus;
+    dump_opp = Lazy.force coq_Ropp;
+    dump_mul = Lazy.force coq_Rmult;
+    dump_pow = Lazy.force coq_Rpower;
+    dump_pow_arg = (fun n -> dump_nat (CamlToCoq.nat (CoqToCaml.n n)));
+    dump_op  = List.map (fun (x,y) -> (y,Lazy.force x)) rop_table
+  }
+
+
+
+
+(** [make_goal_of_formula depxr vars props form] where
+     - vars is an environment for the arithmetic variables occuring in form
+     - props is an environment for the propositions occuring in form
+    @return a goal where all the variables and propositions of the formula are quantified
+
+*)
+
+let prodn n env b =
+  let rec prodrec = function
+    | (0, env, b)        -> b
+    | (n, ((v,t)::l), b) -> prodrec (n-1,  l, EConstr.mkProd (v,t,b))
+    | _ -> assert false
+  in
+  prodrec (n,env,b)
+
+let make_goal_of_formula sigma dexpr form =
+
+  let vars_idx =
+    List.mapi (fun i v -> (v, i+1))  (ISet.elements (var_env_of_formula form)) in
+
+  (*  List.iter (fun (v,i) -> Printf.fprintf stdout "var %i has index %i\n" v i) vars_idx ;*)
+
+  let props     = prop_env_of_formula sigma form in
+
+  let vars_n  = List.map (fun (_,i) -> (Names.Id.of_string (Printf.sprintf "__x%i" i)) , dexpr.interp_typ) vars_idx in
+  let props_n = List.mapi (fun i _ -> (Names.Id.of_string (Printf.sprintf "__p%i" (i+1))) , EConstr.mkProp) props in
+
+  let var_name_pos = List.map2 (fun (idx,_) (id,_) -> id,idx) vars_idx vars_n in
+
+  let  dump_expr i e =
+    let rec dump_expr  = function
+    | Mc.PEX n -> EConstr.mkRel (i+(List.assoc (CoqToCaml.positive n)  vars_idx))
+    | Mc.PEc z -> dexpr.dump_cst z
+    | Mc.PEadd(e1,e2) -> EConstr.mkApp(dexpr.dump_add,
+                               [| dump_expr e1;dump_expr e2|])
+    | Mc.PEsub(e1,e2) -> EConstr.mkApp(dexpr.dump_sub,
+                               [| dump_expr  e1;dump_expr  e2|])
+    | Mc.PEopp e -> EConstr.mkApp(dexpr.dump_opp,
+                                  [| dump_expr  e|])
+    | Mc.PEmul(e1,e2) -> EConstr.mkApp(dexpr.dump_mul,
+                                       [| dump_expr  e1;dump_expr e2|])
+    | Mc.PEpow(e,n) -> EConstr.mkApp(dexpr.dump_pow,
+                                     [| dump_expr  e; dexpr.dump_pow_arg  n|])
+    in dump_expr e in
+
+  let mkop op e1 e2 =
+      try
+        EConstr.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|])
+      with Not_found ->
+        EConstr.mkApp(Lazy.force coq_Eq,[|dexpr.interp_typ ; e1 ;e2|]) in
+
+  let dump_cstr i { Mc.flhs ; Mc.fop ; Mc.frhs } =
+    mkop fop (dump_expr i flhs) (dump_expr i frhs) in
+
+  let rec xdump pi xi f =
+    match f with
+    | TT  -> Lazy.force coq_True
+    | FF  -> Lazy.force coq_False
+    | C(x,y) -> EConstr.mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|])
+    | D(x,y) -> EConstr.mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|])
+    | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y)
+    | N(x) -> EConstr.mkArrow (xdump pi xi x) (Lazy.force coq_False)
+    | A(x,_,_) -> dump_cstr xi x
+    | X(t) -> let idx = Env.get_rank props sigma t in
+              EConstr.mkRel (pi+idx) in
+
+  let nb_vars  = List.length vars_n  in
+  let nb_props = List.length props_n in
+
+  (*  Printf.fprintf stdout "NBProps : %i\n" nb_props ;*)
+
+  let subst_prop p =
+    let idx = Env.get_rank props sigma p in
+    EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i"  idx)) in
+
+  let form' = map_prop subst_prop   form in
+
+  (prodn nb_props (List.map (fun (x,y) -> Name.Name x,y) props_n)
+     (prodn nb_vars (List.map (fun (x,y) -> Name.Name x,y) vars_n)
+        (xdump (List.length vars_n) 0  form)),
+   List.rev props_n, List.rev var_name_pos,form')
+
+  (**
+     * Given a conclusion and a list of affectations, rebuild a term prefixed by
+     * the appropriate letins.
+     * TODO: reverse the list of bindings!
+  *)
+
+  let set l concl =
+   let rec xset acc = function
+    | [] -> acc
+    | (e::l) ->
+       let (name,expr,typ) = e in
+        xset (EConstr.mkNamedLetIn
+               (Names.Id.of_string name)
+               expr typ acc) l in
+    xset concl l
+
+end (**
+      * MODULE END: M
+      *)
+
+open M
+
+let coq_Node =
+ lazy (gen_constant_in_modules "VarMap"
+   [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Node")
+let coq_Leaf =
+ lazy (gen_constant_in_modules "VarMap"
+   [["Coq" ; "micromega" ; "VarMap"];["VarMap"]] "Leaf")
+let coq_Empty =
+ lazy (gen_constant_in_modules "VarMap"
+   [["Coq" ; "micromega" ;"VarMap"];["VarMap"]] "Empty")
+
+let coq_VarMap =
+  lazy (gen_constant_in_modules "VarMap"
+     [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t")
+
+
+let rec dump_varmap typ m =
+  match m with
+  | Mc.Empty -> EConstr.mkApp(Lazy.force coq_Empty,[| typ |])
+  | Mc.Leaf v -> EConstr.mkApp(Lazy.force coq_Leaf,[| typ; v|])
+  | Mc.Node(l,o,r) ->
+    EConstr.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |])
+
+
+let vm_of_list env =
+  match env with
+  | [] -> Mc.Empty
+  | (d,_)::_ ->
+    List.fold_left (fun vm (c,i) ->
+      Mc.vm_add d (CamlToCoq.positive i) c vm) Mc.Empty env
+
+let rec dump_proof_term = function
+  | Micromega.DoneProof -> Lazy.force coq_doneProof
+  | Micromega.RatProof(cone,rst) ->
+    EConstr.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|])
+ | Micromega.CutProof(cone,prf) ->
+    EConstr.mkApp(Lazy.force coq_cutProof,
+	      [| dump_psatz coq_Z dump_z cone ;
+		 dump_proof_term prf|])
+ | Micromega.EnumProof(c1,c2,prfs) ->
+    EConstr.mkApp (Lazy.force coq_enumProof,
+	           [|  dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ;
+		       dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |])
+
+
+let rec size_of_psatz = function
+  | Micromega.PsatzIn _ -> 1
+  | Micromega.PsatzSquare _ -> 1
+  | Micromega.PsatzMulC(_,p) -> 1 + (size_of_psatz p)
+  | Micromega.PsatzMulE(p1,p2) | Micromega.PsatzAdd(p1,p2) -> size_of_psatz p1 + size_of_psatz p2
+  | Micromega.PsatzC _ -> 1
+  | Micromega.PsatzZ   -> 1
+
+let rec size_of_pf = function
+  | Micromega.DoneProof -> 1
+  | Micromega.RatProof(p,a) -> (size_of_pf a) + (size_of_psatz p)
+  | Micromega.CutProof(p,a) -> (size_of_pf a) + (size_of_psatz p)
+  | Micromega.EnumProof(p1,p2,l) -> (size_of_psatz p1) + (size_of_psatz p2) + (List.fold_left (fun acc p -> size_of_pf p + acc) 0 l)
+
+let dump_proof_term t =
+  if debug then  Printf.printf "dump_proof_term %i\n" (size_of_pf t) ;
+  dump_proof_term t
+
+
+
+let pp_q o q = Printf.fprintf o "%a/%a" pp_z q.Micromega.qnum pp_positive q.Micromega.qden
+
+
+let rec pp_proof_term o = function
+  | Micromega.DoneProof -> Printf.fprintf o "D"
+  | Micromega.RatProof(cone,rst) -> Printf.fprintf o "R[%a,%a]" (pp_psatz  pp_z) cone pp_proof_term rst
+  | Micromega.CutProof(cone,rst) -> Printf.fprintf o "C[%a,%a]" (pp_psatz  pp_z) cone pp_proof_term rst
+  | Micromega.EnumProof(c1,c2,rst) ->
+      Printf.fprintf o "EP[%a,%a,%a]"
+	(pp_psatz pp_z) c1 (pp_psatz pp_z) c2
+     (pp_list "[" "]" pp_proof_term) rst
+
+let rec parse_hyps gl parse_arith env tg hyps =
+ match hyps with
+  | [] -> ([],env,tg)
+  | (i,t)::l ->
+     let (lhyps,env,tg) = parse_hyps gl parse_arith env tg l in
+      try
+       let (c,env,tg) = parse_formula gl parse_arith env  tg t in
+	((i,c)::lhyps, env,tg)
+      with e when CErrors.noncritical e -> (lhyps,env,tg)
+       (*(if debug then Printf.printf "parse_arith : %s\n" x);*)
+
+
+(*exception ParseError*)
+
+let parse_goal gl parse_arith env hyps term =
+ (*  try*)
+ let (f,env,tg) = parse_formula gl parse_arith env (Tag.from 0) term in
+ let (lhyps,env,tg) = parse_hyps gl parse_arith env tg hyps in
+  (lhyps,f,env)
+   (*  with Failure x -> raise ParseError*)
+
+(**
+  * The datastructures that aggregate theory-dependent proof values.
+  *)
+type ('synt_c, 'prf) domain_spec = {
+  typ : EConstr.constr; (* is the type of the interpretation domain - Z, Q, R*)
+  coeff : EConstr.constr ; (* is the type of the syntactic coeffs - Z , Q , Rcst *)
+  dump_coeff : 'synt_c -> EConstr.constr ;
+  proof_typ  : EConstr.constr ;
+  dump_proof   : 'prf -> EConstr.constr
+}
+
+let zz_domain_spec  = lazy {
+ typ = Lazy.force coq_Z;
+ coeff = Lazy.force coq_Z;
+ dump_coeff = dump_z ;
+ proof_typ = Lazy.force coq_proofTerm ;
+ dump_proof = dump_proof_term
+}
+
+let qq_domain_spec  = lazy {
+ typ = Lazy.force coq_Q;
+ coeff = Lazy.force coq_Q;
+ dump_coeff = dump_q ;
+ proof_typ = Lazy.force coq_QWitness ;
+ dump_proof = dump_psatz coq_Q dump_q
+}
+
+(** Naive topological sort of constr according to the subterm-ordering *)
+
+(* An element is minimal x is minimal w.r.t y if
+   x <= y or (x and y are incomparable) *)
+
+(**
+  * Instanciate the current Coq goal with a Micromega formula, a varmap, and a
+  * witness.
+  *)
+
+let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*) =
+ (* let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *)
+ let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in
+ let ff  = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
+ let vm = dump_varmap (spec.typ) (vm_of_list env) in
+ (* todo : directly generate the proof term - or generalize before conversion? *)
+  Proofview.Goal.nf_enter begin fun gl ->
+   Tacticals.New.tclTHENLIST
+    [
+     Tactics.change_concl
+    (set
+      [
+       ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
+       ("__varmap", vm, EConstr.mkApp(Lazy.force coq_VarMap, [|spec.typ|]));
+       ("__wit", cert, cert_typ)
+      ]
+      (Tacmach.New.pf_concl gl))
+  ]
+  end
+
+
+(**
+  * The datastructures that aggregate prover attributes.
+  *)
+
+type ('option,'a,'prf) prover = {
+  name : string ; (* name of the prover *)
+ get_option : unit ->'option ; (* find the options of the prover *)
+ prover : 'option * 'a list -> 'prf option ; (* the prover itself *)
+  hyps : 'prf -> ISet.t ; (* extract the indexes of the hypotheses really used in the proof *)
+  compact : 'prf -> (int -> int) -> 'prf ; (* remap the hyp indexes according to function *)
+  pp_prf : out_channel -> 'prf -> unit ;(* pretting printing of proof *)
+  pp_f   : out_channel -> 'a   -> unit (* pretty printing of the formulas (polynomials)*)
+}
+
+
+
+(**
+  * Given a list of provers and a disjunction of atoms, find a proof of any of
+  * the atoms.  Returns an (optional) pair of a proof and a prover
+  * datastructure.
+  *)
+
+let find_witness provers polys1 =
+  let provers = List.map (fun p ->
+    (fun l ->
+      match p.prover (p.get_option (),l) with
+        | None -> None
+        | Some prf -> Some(prf,p)) , p.name) provers in
+  try_any provers (List.map fst polys1)
+
+(**
+  * Given a list of provers and a CNF, find a proof for each of the clauses.
+  * Return the proofs as a list.
+  *)
+
+let witness_list prover l =
+ let rec xwitness_list l =
+  match l with
+   | [] -> Some []
+   | e :: l ->
+      match find_witness prover e  with
+       | None -> None
+       | Some w ->
+	  (match xwitness_list l with
+	   | None -> None
+	   | Some l -> Some (w :: l)
+	  ) in
+  xwitness_list l
+
+let witness_list_tags  = witness_list
+
+(**
+  * Prune the proof object, according to the 'diff' between two cnf formulas.
+  *)
+
+let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
+
+  let compact_proof (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) =
+    let new_cl = List.mapi (fun i (f,_) -> (f,i)) new_cl in
+    let remap i =
+      let formula = try fst (List.nth old_cl i) with Failure _ -> failwith "bad old index" in
+      List.assoc formula new_cl in
+(*    if debug then
+      begin
+        Printf.printf "\ncompact_proof : %a %a %a"
+          (pp_ml_list prover.pp_f) (List.map fst old_cl)
+          prover.pp_prf prf
+          (pp_ml_list prover.pp_f) (List.map fst new_cl)   ;
+          flush stdout
+      end ; *)
+    let res = try prover.compact prf remap with x when CErrors.noncritical x ->
+      if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
+      (* This should not happen -- this is the recovery plan... *)
+      match prover.prover (prover.get_option () ,List.map fst new_cl) with
+        | None -> failwith "proof compaction error"
+        | Some p ->  p
+    in
+    if debug then
+      begin
+        Printf.printf " -> %a\n"
+          prover.pp_prf res ;
+        flush stdout
+      end ;
+    res in
+
+  let is_proof_compatible (old_cl:'cst clause) (prf,prover) (new_cl:'cst clause) =
+    let hyps_idx = prover.hyps prf in
+    let hyps = selecti hyps_idx old_cl in
+      is_sublist Pervasives.(=) hyps new_cl in
+
+  let cnf_res = List.combine cnf_ff res in (* we get pairs clause * proof *)
+
+  List.map (fun x ->
+    let (o,p) = List.find (fun (l,p) -> is_proof_compatible l p x) cnf_res
+    in compact_proof o p x) cnf_ff'
+
+
+(**
+  * "Hide out" tagged atoms of a formula by transforming them into generic
+  * variables. See the Tag module in mutils.ml for more.
+  *)
+
+let abstract_formula hyps f =
+  let rec xabs f =
+    match f with
+      | X c -> X c
+      | A(a,t,term) -> if TagSet.mem t hyps then A(a,t,term) else X(term)
+      | C(f1,f2) ->
+	  (match xabs f1 , xabs f2 with
+	    |   X a1    ,  X a2   -> X (EConstr.mkApp(Lazy.force coq_and, [|a1;a2|]))
+	    |    f1     , f2      -> C(f1,f2) )
+      | D(f1,f2) ->
+	  (match xabs f1 , xabs f2 with
+	    |   X a1    ,  X a2   -> X (EConstr.mkApp(Lazy.force coq_or, [|a1;a2|]))
+	    |    f1     , f2      -> D(f1,f2) )
+      | N(f) ->
+	  (match xabs f with
+	    |   X a    -> X (EConstr.mkApp(Lazy.force coq_not, [|a|]))
+	    |     f     -> N f)
+      | I(f1,hyp,f2) ->
+	  (match xabs f1 , hyp, xabs f2 with
+	    | X a1      , Some _ , af2    ->  af2
+	    | X a1      , None   , X a2   -> X (EConstr.mkArrow a1 a2)
+	    |   af1     ,  _     , af2    -> I(af1,hyp,af2)
+	  )
+      | FF -> FF
+      | TT -> TT
+  in  xabs f
+
+
+(* [abstract_wrt_formula] is used in contexts whre f1 is already an abstraction of f2   *)
+let rec abstract_wrt_formula f1 f2 =
+  match f1 , f2 with
+    | X c  , _   -> X c
+    | A _  , A _ -> f2
+    | C(a,b) , C(a',b') -> C(abstract_wrt_formula a a', abstract_wrt_formula b b')
+    | D(a,b) , D(a',b') -> D(abstract_wrt_formula a a', abstract_wrt_formula b b')
+    | I(a,_,b) , I(a',x,b') -> I(abstract_wrt_formula a a',x, abstract_wrt_formula b b')
+    | FF , FF -> FF
+    | TT , TT -> TT
+    | N x , N y -> N(abstract_wrt_formula x y)
+    |    _    -> failwith "abstract_wrt_formula"
+
+(**
+  * This exception is raised by really_call_csdpcert if Coq's configure didn't
+  * find a CSDP executable.
+  *)
+
+exception CsdpNotFound
+
+
+(**
+  * This is the core of Micromega: apply the prover, analyze the result and
+  * prune unused fomulas, and finally modify the proof state.
+  *)
+
+let formula_hyps_concl hyps concl =
+  List.fold_right
+   (fun (id,f) (cc,ids) ->
+    match f with
+      X _ -> (cc,ids)
+     | _ -> (I(f,Some id,cc), id::ids))
+    hyps (concl,[])
+
+
+let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 gl =
+
+ (* Express the goal as one big implication *)
+ let (ff,ids) = formula_hyps_concl polys1 polys2 in
+
+ (* Convert the aplpication into a (mc_)cnf (a list of lists of formulas) *)
+ let cnf_ff,cnf_ff_tags = cnf negate normalise unsat deduce ff in
+
+ if debug then
+   begin
+     Feedback.msg_notice (Pp.str "Formula....\n") ;
+     let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in
+     let ff = dump_formula formula_typ
+       (dump_cstr spec.typ spec.dump_coeff) ff in
+       Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff);
+       Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff
+   end;
+
+ match witness_list_tags prover cnf_ff with
+  | None -> None
+  | Some res -> (*Printf.printf "\nList %i" (List.length `res); *)
+  let hyps = List.fold_left (fun s (cl,(prf,p)) ->
+    let tags = ISet.fold (fun i s -> let t = snd (List.nth cl i) in
+                                     if debug then (Printf.fprintf stdout "T : %i -> %a" i Tag.pp t) ;
+      (*try*) TagSet.add t s (* with Invalid_argument _ -> s*)) (p.hyps prf) TagSet.empty in
+    TagSet.union s tags) (List.fold_left (fun s i -> TagSet.add i s) TagSet.empty cnf_ff_tags) (List.combine cnf_ff res) in
+
+  if debug then (Printf.printf "TForm : %a\n" pp_formula ff ; flush stdout;
+                 Printf.printf "Hyps : %a\n" (fun o s -> TagSet.fold (fun i _ -> Printf.fprintf o "%a " Tag.pp i) s ()) hyps) ;
+
+  let ff'     = abstract_formula hyps ff in
+  let cnf_ff',_ = cnf negate normalise unsat deduce ff' in
+
+  if debug then
+    begin
+      Feedback.msg_notice (Pp.str "\nAFormula\n") ;
+      let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in
+      let ff' = dump_formula formula_typ
+          (dump_cstr spec.typ spec.dump_coeff) ff' in
+      Feedback.msg_notice (Printer.pr_leconstr_env gl.env gl.sigma ff');
+      Printf.fprintf stdout "cnf : %a\n" (pp_cnf (fun o _ -> ())) cnf_ff'
+    end;
+
+  (* Even if it does not work, this does not mean it is not provable
+  -- the prover is REALLY incomplete *)
+  (* if debug then
+      begin
+        (* recompute the proofs *)
+        match witness_list_tags prover  cnf_ff' with
+          | None -> failwith "abstraction is wrong"
+          | Some res -> ()
+      end ; *)
+  let res' = compact_proofs cnf_ff res cnf_ff' in
+
+  let (ff',res',ids) = (ff',res', ids_of_formula ff') in
+
+  let res' = dump_list (spec.proof_typ) spec.dump_proof res' in
+    Some (ids,ff',res')
+
+
+(**
+  * Parse the proof environment, and call micromega_tauto
+  *)
+
+let fresh_id avoid id gl =
+  Tactics.fresh_id_in_env avoid id (Proofview.Goal.env gl)
+
+let micromega_gen
+    parse_arith
+    (negate:'cst atom -> 'cst mc_cnf)
+    (normalise:'cst atom -> 'cst mc_cnf)
+    unsat deduce
+    spec dumpexpr prover tac =
+ Proofview.Goal.nf_enter begin fun gl ->
+    let sigma = Tacmach.New.project gl in
+    let concl = Tacmach.New.pf_concl gl in
+    let hyps  = Tacmach.New.pf_hyps_types gl in
+    try
+     let gl0 = { env = Tacmach.New.pf_env gl; sigma } in
+     let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in
+     let env = Env.elements env in
+     let spec = Lazy.force spec in
+     let dumpexpr = Lazy.force dumpexpr in
+
+     match micromega_tauto  negate normalise unsat deduce spec prover env hyps concl gl0 with
+     | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness")
+     | Some (ids,ff',res') ->
+       let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma dumpexpr ff' in
+       let intro (id,_) = Tactics.introduction id  in
+
+       let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
+       let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
+       let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in
+       let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in
+       let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in
+
+       let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ;
+                                                    micromega_order_change spec res'
+                                                      (EConstr.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in
+
+       let goal_props = List.rev (prop_env_of_formula sigma ff') in
+
+       let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in
+
+       let arith_args = goal_props @ goal_vars in
+
+       let kill_arith =
+           Tacticals.New.tclTHEN
+             (Tactics.keep [])
+             ((*Tactics.tclABSTRACT  None*)
+                (Tacticals.New.tclTHEN tac_arith tac)) in
+
+       Tacticals.New.tclTHENS
+         (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal)
+         [
+           kill_arith;
+           (Tacticals.New.tclTHENLIST
+            [(Tactics.generalize (List.map EConstr.mkVar ids));
+             Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args))
+            ] )
+         ]
+    with
+    | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
+    | Mfourier.TimeOut  -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
+    | CsdpNotFound -> flush stdout ;
+     Tacticals.New.tclFAIL 0 (Pp.str
+                           (" Skipping what remains of this tactic: the complexity of the goal requires "
+                            ^ "the use of a specialized external tool called csdp. \n\n"
+                            ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
+                            ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
+  end
+
+let micromega_gen parse_arith
+    (negate:'cst atom -> 'cst mc_cnf)
+    (normalise:'cst atom -> 'cst mc_cnf)
+    unsat deduce
+    spec prover  =
+ (micromega_gen parse_arith negate normalise unsat deduce spec prover)
+
+
+
+let micromega_order_changer cert env ff  =
+  (*let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *)
+  let coeff = Lazy.force coq_Rcst in
+  let dump_coeff = dump_Rcst in
+  let typ  = Lazy.force coq_R in
+  let cert_typ = (EConstr.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in
+
+  let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
+  let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
+  let vm = dump_varmap (typ) (vm_of_list env) in
+  Proofview.Goal.nf_enter begin fun gl ->
+    Tacticals.New.tclTHENLIST
+     [
+     (Tactics.change_concl
+      (set
+        [
+         ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
+         ("__varmap", vm, EConstr.mkApp
+          (gen_constant_in_modules "VarMap"
+	    [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|]));
+         ("__wit", cert, cert_typ)
+        ]
+        (Tacmach.New.pf_concl gl)));
+     (*      Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)*)
+     ]
+  end
+
+let micromega_genr prover tac =
+  let parse_arith = parse_rarith in
+  let negate = Mc.rnegate in
+  let normalise = Mc.rnormalise in
+  let unsat = Mc.runsat in
+  let deduce = Mc.rdeduce in
+  let spec = lazy {
+    typ = Lazy.force coq_R;
+    coeff = Lazy.force coq_Rcst;
+    dump_coeff = dump_q;
+    proof_typ = Lazy.force coq_QWitness ;
+    dump_proof = dump_psatz coq_Q dump_q
+  } in
+  Proofview.Goal.nf_enter begin fun gl ->
+     let sigma = Tacmach.New.project gl in
+     let concl = Tacmach.New.pf_concl gl in
+     let hyps  = Tacmach.New.pf_hyps_types gl in
+
+     try
+      let gl0 = { env = Tacmach.New.pf_env gl; sigma } in
+      let (hyps,concl,env) = parse_goal gl0 parse_arith Env.empty hyps concl in
+       let env = Env.elements env in
+       let spec = Lazy.force spec in
+
+       let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in
+       let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in
+
+       match micromega_tauto  negate normalise unsat deduce spec prover env hyps' concl' gl0 with
+       | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness")
+       | Some (ids,ff',res') ->
+         let (ff,ids) = formula_hyps_concl
+	     (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in
+         let ff' = abstract_wrt_formula ff' ff  in
+
+         let (arith_goal,props,vars,ff_arith) = make_goal_of_formula sigma (Lazy.force dump_rexpr)  ff' in
+         let intro (id,_) = Tactics.introduction id  in
+
+       let intro_vars = Tacticals.New.tclTHENLIST (List.map intro vars) in
+       let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in
+       let ipat_of_name id = Some (CAst.make @@ IntroNaming (Namegen.IntroIdentifier id)) in
+       let goal_name = fresh_id Id.Set.empty (Names.Id.of_string "__arith") gl in
+       let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in
+
+       let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ;
+                                                    micromega_order_changer res' env' ff_arith ] in
+
+       let goal_props = List.rev (prop_env_of_formula sigma ff') in
+
+       let goal_vars = List.map (fun (_,i) -> List.nth env (i-1)) vars in
+
+       let arith_args = goal_props @ goal_vars in
+
+       let kill_arith =
+           Tacticals.New.tclTHEN
+             (Tactics.keep [])
+             ((*Tactics.tclABSTRACT  None*)
+                (Tacticals.New.tclTHEN tac_arith tac)) in
+
+       Tacticals.New.tclTHENS
+         (Tactics.forward true (Some None) (ipat_of_name goal_name) arith_goal)
+         [
+           kill_arith;
+           (Tacticals.New.tclTHENLIST
+            [(Tactics.generalize (List.map EConstr.mkVar ids));
+             Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args))
+            ] )
+         ]
+
+    with
+    | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
+    | Mfourier.TimeOut  -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
+    | CsdpNotFound -> flush stdout ;
+     Tacticals.New.tclFAIL 0 (Pp.str
+                           (" Skipping what remains of this tactic: the complexity of the goal requires "
+                            ^ "the use of a specialized external tool called csdp. \n\n"
+                            ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
+                            ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
+  end
+
+
+
+
+let micromega_genr prover  = (micromega_genr prover)
+
+
+let lift_ratproof  prover l =
+ match prover l with
+  | None -> None
+  | Some c -> Some (Mc.RatProof( c,Mc.DoneProof))
+
+type micromega_polys = (Micromega.q Mc.pol * Mc.op1) list
+
+[@@@ocaml.warning "-37"]
+type csdp_certificate = S of Sos_types.positivstellensatz option | F of string
+(* Used to read the result of the execution of csdpcert *)
+
+type provername = string * int option
+
+(**
+  * The caching mechanism.
+  *)
+
+open Micromega_plugin.Persistent_cache
+
+module Cache = PHashtable(struct
+  type t = (provername * micromega_polys)
+  let equal = Pervasives.(=)
+  let hash  = Hashtbl.hash
+end)
+
+let csdp_cache = ".csdp.cache"
+
+(**
+  * Build the command to call csdpcert, and launch it. This in turn will call
+  * the sos driver to the csdp executable.
+  * Throw CsdpNotFound if Coq isn't aware of any csdp executable.
+  *)
+
+let require_csdp =
+  if System.is_in_system_path "csdp"
+  then lazy ()
+  else lazy (raise CsdpNotFound)
+
+let really_call_csdpcert : provername -> micromega_polys -> Sos_types.positivstellensatz option  =
+  fun provername poly ->
+
+  Lazy.force require_csdp;
+
+  let cmdname =
+    List.fold_left Filename.concat (Envars.coqlib ())
+      ["plugins"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
+
+    match ((command cmdname [|cmdname|] (provername,poly)) : csdp_certificate) with
+      | F str -> failwith str
+      | S res -> res
+
+(**
+  * Check the cache before calling the prover.
+  *)
+
+let xcall_csdpcert =
+  Cache.memo csdp_cache (fun (prover,pb) -> really_call_csdpcert prover pb)
+
+(**
+  * Prover callback functions.
+  *)
+
+let call_csdpcert prover pb = xcall_csdpcert (prover,pb)
+
+let rec z_to_q_pol e =
+ match e with
+  | Mc.Pc z   -> Mc.Pc {Mc.qnum = z ; Mc.qden = Mc.XH}
+  | Mc.Pinj(p,pol)   -> Mc.Pinj(p,z_to_q_pol pol)
+  | Mc.PX(pol1,p,pol2) -> Mc.PX(z_to_q_pol pol1, p, z_to_q_pol pol2)
+
+let call_csdpcert_q provername poly =
+ match call_csdpcert provername poly with
+  | None -> None
+  | Some cert ->
+     let cert = Certificate.q_cert_of_pos cert in
+     if Mc.qWeakChecker poly cert
+     then Some cert
+     else ((print_string "buggy certificate") ;None)
+
+let call_csdpcert_z provername poly =
+ let l = List.map (fun (e,o) -> (z_to_q_pol e,o)) poly in
+  match call_csdpcert provername l with
+   | None -> None
+   | Some cert ->
+      let cert = Certificate.z_cert_of_pos cert in
+      if Mc.zWeakChecker poly cert
+      then Some cert
+      else ((print_string "buggy certificate" ; flush stdout) ;None)
+
+let xhyps_of_cone base acc prf =
+  let rec xtract e acc =
+    match e with
+    | Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> acc
+    | Mc.PsatzIn n -> let n = (CoqToCaml.nat n) in
+			if n >= base
+			then  ISet.add (n-base) acc
+			else acc
+    | Mc.PsatzMulC(_,c) -> xtract  c acc
+    | Mc.PsatzAdd(e1,e2) |  Mc.PsatzMulE(e1,e2) -> xtract e1 (xtract e2 acc) in
+
+    xtract prf acc
+
+let hyps_of_cone prf = xhyps_of_cone 0 ISet.empty prf
+
+let compact_cone prf f  =
+  let np n = CamlToCoq.nat (f (CoqToCaml.nat n)) in
+
+  let rec xinterp prf =
+    match prf with
+    | Mc.PsatzC _ | Mc.PsatzZ | Mc.PsatzSquare _ -> prf
+    | Mc.PsatzIn n -> Mc.PsatzIn (np n)
+    | Mc.PsatzMulC(e,c) -> Mc.PsatzMulC(e,xinterp c)
+    | Mc.PsatzAdd(e1,e2) -> Mc.PsatzAdd(xinterp e1,xinterp e2)
+    | Mc.PsatzMulE(e1,e2) -> Mc.PsatzMulE(xinterp e1,xinterp e2) in
+
+    xinterp prf
+
+let hyps_of_pt pt =
+
+  let rec xhyps base pt acc =
+    match pt with
+      | Mc.DoneProof -> acc
+      | Mc.RatProof(c,pt) ->  xhyps (base+1) pt (xhyps_of_cone base acc c)
+      | Mc.CutProof(c,pt) -> xhyps (base+1) pt (xhyps_of_cone base acc c)
+      | Mc.EnumProof(c1,c2,l) ->
+	  let s = xhyps_of_cone base (xhyps_of_cone base acc c2) c1 in
+	    List.fold_left (fun s x -> xhyps (base + 1) x s) s l in
+
+    xhyps 0 pt ISet.empty
+
+let hyps_of_pt pt =
+  let res = hyps_of_pt pt in
+    if debug
+    then (Printf.fprintf stdout "\nhyps_of_pt : %a -> " pp_proof_term pt ; ISet.iter (fun i -> Printf.printf "%i " i) res);
+    res
+
+let compact_pt pt f =
+  let translate ofset x =
+    if x < ofset then x
+    else (f (x-ofset) + ofset) in
+
+  let rec compact_pt ofset pt =
+    match pt with
+      | Mc.DoneProof -> Mc.DoneProof
+      | Mc.RatProof(c,pt) -> Mc.RatProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt )
+      | Mc.CutProof(c,pt) -> Mc.CutProof(compact_cone c (translate (ofset)), compact_pt (ofset+1) pt )
+      | Mc.EnumProof(c1,c2,l) -> Mc.EnumProof(compact_cone c1 (translate (ofset)), compact_cone c2 (translate (ofset)),
+						   Mc.map (fun x -> compact_pt (ofset+1) x) l) in
+    compact_pt 0 pt
+
+(**
+  * Definition of provers.
+  * Instantiates the type ('a,'prf) prover defined above.
+  *)
+
+let lift_pexpr_prover p l =  p (List.map (fun (e,o) -> Mc.denorm e , o) l)
+
+module CacheZ = PHashtable(struct
+ type prover_option = bool * int
+
+ type t = prover_option * ((Mc.z Mc.pol * Mc.op1) list)
+  let equal = (=)
+  let hash  = Hashtbl.hash
+end)
+
+module CacheQ = PHashtable(struct
+  type t = int * ((Mc.q Mc.pol * Mc.op1) list)
+  let equal = (=)
+  let hash  = Hashtbl.hash
+end)
+
+let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s)
+let memo_nlia = CacheZ.memo ".nia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s)
+let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s)
+
+
+
+let linear_prover_Q = {
+ name    = "linear prover";
+ get_option = get_lra_option ;
+ prover  = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ;
+ hyps    = hyps_of_cone ;
+ compact = compact_cone ;
+ pp_prf  = pp_psatz pp_q ;
+ pp_f   = fun o x -> pp_pol pp_q o  (fst x)
+}
+
+
+let linear_prover_R = {
+  name    = "linear prover";
+ get_option = get_lra_option ;
+ prover  = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ;
+  hyps    = hyps_of_cone ;
+  compact = compact_cone ;
+  pp_prf  = pp_psatz pp_q ;
+  pp_f    =  fun o x -> pp_pol pp_q o (fst x)
+}
+
+let nlinear_prover_R = {
+  name    = "nra";
+ get_option = get_lra_option;
+ prover  = memo_nra ;
+  hyps    = hyps_of_cone ;
+  compact = compact_cone ;
+  pp_prf  = pp_psatz pp_q ;
+  pp_f    =  fun o x -> pp_pol pp_q o (fst x)
+}
+
+let non_linear_prover_Q str o = {
+  name    = "real nonlinear prover";
+ get_option = (fun () -> (str,o));
+ prover  = (fun (o,l) -> call_csdpcert_q o l);
+  hyps    = hyps_of_cone;
+  compact = compact_cone ;
+  pp_prf  = pp_psatz pp_q ;
+  pp_f    = fun o x -> pp_pol pp_q o  (fst x)
+}
+
+let non_linear_prover_R str o = {
+  name    = "real nonlinear prover";
+ get_option = (fun () -> (str,o));
+ prover  = (fun (o,l) -> call_csdpcert_q o l);
+  hyps    = hyps_of_cone;
+  compact = compact_cone;
+  pp_prf  = pp_psatz pp_q;
+  pp_f    = fun o x -> pp_pol pp_q o  (fst x)
+}
+
+let non_linear_prover_Z str o  = {
+  name    = "real nonlinear prover";
+ get_option = (fun () -> (str,o));
+ prover  = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l);
+  hyps    = hyps_of_pt;
+  compact = compact_pt;
+  pp_prf  = pp_proof_term;
+  pp_f    =  fun o x -> pp_pol pp_z o (fst x)
+}
+
+let linear_Z =   {
+  name    = "lia";
+ get_option = get_lia_option;
+ prover  = memo_zlinear_prover ;
+  hyps    = hyps_of_pt;
+  compact = compact_pt;
+  pp_prf  = pp_proof_term;
+  pp_f    = fun o x -> pp_pol pp_z o (fst x)
+}
+
+let nlinear_Z =   {
+  name    = "nlia";
+ get_option = get_lia_option;
+ prover  = memo_nlia ;
+  hyps    = hyps_of_pt;
+  compact = compact_pt;
+  pp_prf  = pp_proof_term;
+  pp_f    = fun o x -> pp_pol pp_z o (fst x)
+}
+
+(**
+  * Functions instantiating micromega_gen with the appropriate theories and
+  * solvers
+  *)
+
+let lra_Q =
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
+  [ linear_prover_Q ]
+
+let psatz_Q i  =
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
+  [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ]
+
+let lra_R  =
+ micromega_genr [ linear_prover_R ]
+
+let psatz_R i  =
+ micromega_genr  [ non_linear_prover_R "real_nonlinear_prover" (Some i) ]
+
+
+let psatz_Z i  =
+    micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
+      [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ]
+
+let sos_Z  =
+ micromega_gen parse_zarith Mc.negate Mc.normalise  Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
+  [ non_linear_prover_Z "pure_sos" None ]
+
+let sos_Q  =
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise  Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
+  [ non_linear_prover_Q "pure_sos" None ]
+
+
+let sos_R  =
+ micromega_genr  [ non_linear_prover_R "pure_sos" None ]
+
+
+let xlia  =  micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
+      [ linear_Z ]
+
+let xnlia  =
+    micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec dump_zexpr
+      [ nlinear_Z ]
+
+let nra  =
+ micromega_genr  [ nlinear_prover_R ]
+
+let nqa  =
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec dump_qexpr
+  [ nlinear_prover_R ]
+
+
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/src/versions/standard/mutils_full.ml b/src/versions/standard/mutils_full.ml
new file mode 100644
index 0000000..efa2e4d
--- /dev/null
+++ b/src/versions/standard/mutils_full.ml
@@ -0,0 +1,358 @@
+(*** This file is taken from Coq-8.9.0 to solve a compilation issue due
+   to a wrong order in dependencies.
+   See https://github.com/coq/coq/issues/9768 . ***)
+
+
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(* ** Utility functions **                                              *)
+(*                                                                      *)
+(* - Modules CoqToCaml, CamlToCoq                                       *)
+(* - Modules Cmp, Tag, TagSet                                           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*                                                                      *)
+(************************************************************************)
+
+module Micromega = Micromega_plugin.Micromega
+
+let rec pp_list f o l =
+  match l with
+    | [] -> ()
+    | e::l -> f o e ; output_string o ";" ; pp_list f o l
+
+
+let finally f rst =
+  try
+    let res = f () in
+      rst () ; res
+  with reraise ->
+    (try rst ()
+    with any -> raise reraise
+    ); raise reraise
+
+let rec try_any l x =
+ match l with
+  | [] -> None
+  | (f,s)::l -> match f x with
+     | None -> try_any l x
+     | x -> x
+
+let all_sym_pairs f l = 
+  let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in
+
+  let rec xpairs acc l = 
+    match l with
+      | [] -> acc
+      | e::l -> xpairs (pair_with acc e l) l in
+    xpairs [] l
+
+let all_pairs f l = 
+  let pair_with acc e l = List.fold_left (fun acc x -> (f e x) ::acc) acc l in
+
+  let rec xpairs acc l = 
+    match l with
+      | [] -> acc
+      | e::lx -> xpairs (pair_with acc e l) lx in
+    xpairs [] l
+
+let rec is_sublist f l1 l2 =
+  match l1 ,l2 with
+    | [] ,_ -> true
+    | e::l1', [] -> false
+    | e::l1' , e'::l2' ->
+	if f e e' then is_sublist f l1' l2'
+	else is_sublist f l1 l2'
+
+let extract pred l = 
+  List.fold_left (fun (fd,sys) e -> 
+		    match fd with
+		    | None -> 
+			begin
+			  match pred e with
+			  | None -> fd, e::sys
+			  | Some v -> Some(v,e) , sys
+			end
+		    |  _   -> (fd, e::sys)
+		 ) (None,[]) l
+
+open Num
+open Big_int
+
+let ppcm x y =
+ let g = gcd_big_int x y in
+ let x' = div_big_int x g in
+ let y' = div_big_int y g in
+  mult_big_int g (mult_big_int x' y')
+
+let denominator = function
+ | Int _ | Big_int _ -> unit_big_int
+ | Ratio r -> Ratio.denominator_ratio r
+
+let numerator = function
+ | Ratio r -> Ratio.numerator_ratio r
+ | Int i -> Big_int.big_int_of_int i
+ | Big_int i -> i
+
+let rec ppcm_list c l =
+ match l with
+  | [] -> c
+  | e::l -> ppcm_list (ppcm c (denominator e)) l
+
+let rec rec_gcd_list c l  =
+ match l with
+  | [] -> c
+  | e::l -> rec_gcd_list (gcd_big_int  c (numerator e)) l
+
+let gcd_list l =
+ let res = rec_gcd_list zero_big_int l in
+  if Int.equal (compare_big_int res zero_big_int) 0
+  then unit_big_int else res
+
+let rats_to_ints l =
+ let c = ppcm_list unit_big_int l in
+  List.map (fun x ->  (div_big_int (mult_big_int (numerator x) c)
+			(denominator x))) l
+
+(* assoc_pos j [a0...an] = [j,a0....an,j+n],j+n+1 *)
+(**
+  * MODULE: Coq to Caml data-structure mappings
+  *)
+
+module CoqToCaml =
+struct
+ open Micromega
+
+ let rec nat = function
+  | O -> 0
+  | S n -> (nat n) + 1
+
+
+ let rec positive p =
+  match p with
+   | XH -> 1
+   | XI p -> 1+ 2*(positive p)
+   | XO p -> 2*(positive p)
+
+ let n nt =
+  match nt with
+   | N0 -> 0
+   | Npos p -> positive p
+
+ let rec index i = (* Swap left-right ? *)
+  match i with
+   | XH -> 1
+   | XI i -> 1+(2*(index i))
+   | XO i -> 2*(index i)
+
+ open Big_int
+
+ let rec positive_big_int p =
+  match p with
+   | XH -> unit_big_int
+   | XI p -> add_int_big_int 1 (mult_int_big_int 2 (positive_big_int p))
+   | XO p -> (mult_int_big_int 2 (positive_big_int p))
+
+ let z_big_int x =
+  match x with
+   | Z0 -> zero_big_int
+   | Zpos p -> (positive_big_int p)
+   | Zneg p -> minus_big_int (positive_big_int p)
+
+ let q_to_num {qnum = x ; qden = y} =
+  Big_int (z_big_int x) // (Big_int (z_big_int (Zpos y)))
+
+end
+
+
+(**
+  * MODULE: Caml to Coq data-structure mappings
+  *)
+
+module CamlToCoq =
+struct
+ open Micromega
+
+ let rec nat = function
+  | 0 -> O
+  | n -> S (nat (n-1))
+
+
+ let rec positive n =
+  if Int.equal n 1 then XH
+  else if Int.equal (n land 1) 1 then XI (positive (n lsr 1))
+  else  XO (positive (n lsr 1))
+
+ let n nt =
+  if nt < 0
+  then assert false
+  else if Int.equal nt 0 then N0
+  else Npos (positive nt)
+
+ let rec index  n =
+  if Int.equal n 1 then XH
+  else if Int.equal (n land 1) 1 then XI (index (n lsr 1))
+  else  XO (index (n lsr 1))
+
+
+ let z x =
+  match compare x 0 with
+   | 0 -> Z0
+   | 1 -> Zpos (positive x)
+   | _ -> (* this should be -1 *)
+      Zneg (positive (-x))
+
+ open Big_int
+
+ let positive_big_int n =
+  let two = big_int_of_int 2 in
+  let rec _pos n =
+   if eq_big_int n unit_big_int then XH
+   else
+    let (q,m) = quomod_big_int n two  in
+     if eq_big_int unit_big_int m
+     then XI (_pos q)
+     else XO (_pos q) in
+   _pos n
+
+ let bigint x =
+  match sign_big_int x with
+   | 0 -> Z0
+   | 1 -> Zpos (positive_big_int x)
+   | _ -> Zneg (positive_big_int (minus_big_int x))
+
+ let q n =
+  {Micromega.qnum = bigint (numerator n) ;
+   Micromega.qden = positive_big_int (denominator n)}
+
+end
+
+(**
+  * MODULE: Comparisons on lists: by evaluating the elements in a single list,
+  * between two lists given an ordering, and using a hash computation
+  *)
+
+module Cmp =
+struct
+
+ let rec compare_lexical l =
+  match l with
+   | [] -> 0 (* Equal *)
+   | f::l ->
+      let cmp = f () in
+       if Int.equal cmp 0 then compare_lexical l else cmp
+
+ let rec compare_list cmp l1 l2 =
+  match l1 , l2 with
+   | []  , [] -> 0
+   | []  , _  -> -1
+   | _   , [] -> 1
+   | e1::l1 , e2::l2 ->
+      let c = cmp e1 e2 in
+       if Int.equal c 0 then compare_list cmp l1 l2 else c
+
+end
+
+(**
+  * MODULE: Labels for atoms in propositional formulas. 
+  * Tags are used to identify unused atoms in CNFs, and propagate them back to
+  * the original formula. The translation back to Coq then ignores these
+  * superfluous items, which speeds the translation up a bit.
+  *)
+
+module type Tag =
+sig
+
+  type t
+
+  val from : int -> t
+  val next : t -> t
+  val pp : out_channel -> t -> unit
+  val compare : t -> t -> int
+
+end
+
+module Tag : Tag =
+struct
+
+  type t = int
+
+  let from i = i
+  let next i = i + 1
+  let pp o i = output_string o (string_of_int i)
+  let compare : int -> int -> int = Int.compare
+
+end
+
+(**
+  * MODULE: Ordered sets of tags.
+  *)
+
+module TagSet = Set.Make(Tag)
+
+(** As for Unix.close_process, our Unix.waipid will ignore all EINTR *)
+
+let rec waitpid_non_intr pid =
+  try snd (Unix.waitpid [] pid)
+  with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_non_intr pid
+
+(**
+  * Forking routine, plumbing the appropriate pipes where needed.
+  *)
+
+let command exe_path args vl =
+  (* creating pipes for stdin, stdout, stderr *)
+  let (stdin_read,stdin_write) = Unix.pipe ()
+  and (stdout_read,stdout_write) = Unix.pipe ()
+  and (stderr_read,stderr_write) = Unix.pipe () in
+
+  (* Create the process *)
+  let pid = Unix.create_process exe_path args stdin_read stdout_write stderr_write in
+
+  (* Write the data on the stdin of the created process *)
+  let outch = Unix.out_channel_of_descr stdin_write in
+    output_value outch vl ;
+    flush outch ;
+
+  (* Wait for its completion *)
+    let status = waitpid_non_intr pid in
+
+      finally
+        (* Recover the result *)
+	(fun () ->
+	  match status with
+	    | Unix.WEXITED 0 ->
+		let inch = Unix.in_channel_of_descr stdout_read in
+		begin
+                  try Marshal.from_channel inch
+                  with any ->
+                    failwith
+                      (Printf.sprintf "command \"%s\" exited %s" exe_path
+                         (Printexc.to_string any))
+                end
+	    | Unix.WEXITED i   ->
+                failwith (Printf.sprintf "command \"%s\" exited %i" exe_path i)
+	    | Unix.WSIGNALED i ->
+                failwith (Printf.sprintf "command \"%s\" killed %i" exe_path i)
+	    | Unix.WSTOPPED i  ->
+                failwith (Printf.sprintf "command \"%s\" stopped %i" exe_path i))
+        (* Cleanup  *)
+	(fun () ->
+	  List.iter (fun x -> try Unix.close x with any -> ())
+            [stdin_read; stdin_write;
+             stdout_read; stdout_write;
+             stderr_read; stderr_write])
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/src/versions/standard/mutils_full.mli b/src/versions/standard/mutils_full.mli
new file mode 100644
index 0000000..d506485
--- /dev/null
+++ b/src/versions/standard/mutils_full.mli
@@ -0,0 +1,77 @@
+(*** This file is taken from Coq-8.9.0 to solve a compilation issue due
+   to a wrong order in dependencies.
+   See https://github.com/coq/coq/issues/9768 . ***)
+
+
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+module Micromega = Micromega_plugin.Micromega
+
+val numerator : Num.num -> Big_int.big_int
+val denominator : Num.num -> Big_int.big_int
+
+module Cmp : sig
+
+  val compare_list : ('a -> 'b -> int) -> 'a list -> 'b list -> int
+  val compare_lexical : (unit -> int) list -> int
+
+end
+
+module Tag : sig
+
+  type t
+
+  val pp : out_channel -> t -> unit
+  val next : t -> t
+  val from : int -> t
+
+end
+
+module TagSet : CSig.SetS with type elt = Tag.t
+
+val pp_list : (out_channel -> 'a -> unit) -> out_channel -> 'a list -> unit
+
+module CamlToCoq : sig
+
+  val positive : int -> Micromega.positive
+  val bigint : Big_int.big_int -> Micromega.z
+  val n : int -> Micromega.n
+  val nat : int -> Micromega.nat
+  val q : Num.num -> Micromega.q
+  val index : int -> Micromega.positive
+  val z : int -> Micromega.z
+  val positive_big_int : Big_int.big_int -> Micromega.positive
+
+end
+
+module CoqToCaml : sig
+
+  val z_big_int : Micromega.z -> Big_int.big_int
+  val q_to_num : Micromega.q -> Num.num
+  val positive : Micromega.positive -> int
+  val n : Micromega.n -> int
+  val nat : Micromega.nat -> int
+  val index : Micromega.positive -> int
+
+end
+
+val rats_to_ints : Num.num list -> Big_int.big_int list
+
+val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list
+val all_sym_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list
+val try_any : (('a -> 'b option) * 'c) list -> 'a -> 'b option
+val is_sublist : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
+
+val gcd_list : Num.num list -> Big_int.big_int
+
+val extract : ('a -> 'b option) -> 'a list -> ('b * 'a) option * 'a list
+
+val command : string -> string array -> 'a -> 'b
diff --git a/src/versions/standard/smtcoq_plugin_standard.mlpack b/src/versions/standard/smtcoq_plugin_standard.mlpack
index 68ce13a..0101147 100644
--- a/src/versions/standard/smtcoq_plugin_standard.mlpack
+++ b/src/versions/standard/smtcoq_plugin_standard.mlpack
@@ -1,3 +1,5 @@
+Mutils_full
+Coq_micromega_full
 Structures
 
 SmtMisc
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index f259a70..ea35a35 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -77,14 +77,14 @@ let mkTConst c noc ty =
 
 (* TODO : Set -> Type *)
 let declare_new_type t =
-  let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_const_entry Univ.ContextSet.empty) Universes.empty_binders [] false Vernacexpr.NoInline (CAst.make t) in
+  let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_const_entry Univ.ContextSet.empty) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in
   Constr.mkVar t
 
 let declare_new_variable v constr_t =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let evd, _ = Typing.type_of env evd (EConstr.of_constr constr_t) in
-  let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.const_univ_entry ~poly:false evd) Universes.empty_binders [] false Vernacexpr.NoInline (CAst.make v) in
+  let _ = ComAssumption.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.const_univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in
   Constr.mkVar v
 
 let declare_constant n c =
@@ -103,7 +103,7 @@ let econstr_of_constr = EConstr.of_constr
 
 
 (* Modules *)
-let gen_constant_in_modules s m n = Universes.constr_of_global @@ Coqlib.gen_reference_in_modules s m n
+let gen_constant_in_modules s m n = UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n
 let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
 
 
@@ -165,18 +165,18 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r =
 
 
 (* Micromega *)
-module Micromega_plugin_Certificate = Micromega_plugin.Certificate
-module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega
 module Micromega_plugin_Micromega = Micromega_plugin.Micromega
-module Micromega_plugin_Mutils = Micromega_plugin.Mutils
+module Micromega_plugin_Mutils = Mutils_full
+module Micromega_plugin_Certificate = Micromega_plugin.Certificate
+module Micromega_plugin_Coq_micromega = Coq_micromega_full
 
 let micromega_coq_proofTerm =
   (* Cannot contain evars *)
-  lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin.Coq_micromega.M.coq_proofTerm)))
+  lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin_Coq_micromega.M.coq_proofTerm)))
 
 let micromega_dump_proof_term p =
   (* Cannot contain evars *)
-  EConstr.Unsafe.to_constr (Micromega_plugin.Coq_micromega.dump_proof_term p)
+  EConstr.Unsafe.to_constr (Micromega_plugin_Coq_micromega.dump_proof_term p)
 
 
 (* Tactics *)
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index 3d6f6b2..3aa8b3b 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -87,13 +87,13 @@ val mkTrace :
 
 
 (* Micromega *)
-module Micromega_plugin_Certificate = Micromega_plugin.Certificate
-module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega
 module Micromega_plugin_Micromega = Micromega_plugin.Micromega
-module Micromega_plugin_Mutils = Micromega_plugin.Mutils
+module Micromega_plugin_Mutils = Mutils_full
+module Micromega_plugin_Certificate = Micromega_plugin.Certificate
+module Micromega_plugin_Coq_micromega = Coq_micromega_full
 
 val micromega_coq_proofTerm : constr lazy_t
-val micromega_dump_proof_term : Micromega_plugin_Certificate.Mc.zArithProof -> constr
+val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr
 
 
 (* Tactics *)
@@ -110,11 +110,11 @@ val set_evars_tac : constr -> tactic
 type constr_expr = Constrexpr.constr_expr
 val error : string -> 'a
 val extern_constr : constr -> constr_expr
-val destruct_rel_decl : Context.Rel.Declaration.t -> name * constr
+val destruct_rel_decl : (constr, types) Context.Rel.Declaration.pt -> name * types
 val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr
-val ppconstr_lsimpleconstr : Notation_term.tolerability
+val ppconstr_lsimpleconstr : Notation_gram.tolerability
 val constrextern_extern_constr : constr -> constr_expr
-val get_rel_dec_name : Context.Rel.Declaration.t -> name
+val get_rel_dec_name : (constr, types) Context.Rel.Declaration.pt -> name
 val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr
 
 val vm_conv : Reduction.conv_pb -> types Reduction.kernel_conversion_function