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

17 files changed, 2735 insertions, 47 deletions

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