Port to coq-8.10 under progress

13 files changed, 71 insertions, 2720 deletions

diff --git a/src/trace/coqTerms.ml b/src/trace/coqTerms.ml
index ad5ec1d..a1b6765 100644
--- a/src/trace/coqTerms.ml
+++ b/src/trace/coqTerms.ml
@@ -10,7 +10,6 @@
 (**************************************************************************)
 
 
-open Coqlib
 open SmtMisc
 
 
@@ -25,9 +24,9 @@ let ceq63 = gen_constant Structures.int63_modules "eqb"
 let carray = gen_constant Structures.parray_modules "array"
 
 (* nat *)
-let cnat = gen_constant init_modules "nat"
-let cO = gen_constant init_modules "O"
-let cS = gen_constant init_modules "S"
+let cnat = gen_constant Structures.init_modules "nat"
+let cO = gen_constant Structures.init_modules "O"
+let cS = gen_constant Structures.init_modules "S"
 
 (* Positive *)
 let positive_modules = [["Coq";"Numbers";"BinNums"];
@@ -72,49 +71,49 @@ let ceqbZ = gen_constant z_modules "eqb"
 (* Booleans *)
 let bool_modules = [["Coq";"Bool";"Bool"]]
 
-let cbool = gen_constant init_modules "bool"
-let ctrue = gen_constant init_modules "true"
-let cfalse = gen_constant init_modules "false"
-let candb = gen_constant init_modules "andb"
-let corb = gen_constant init_modules "orb"
-let cxorb = gen_constant init_modules "xorb"
-let cnegb = gen_constant init_modules "negb"
-let cimplb = gen_constant init_modules "implb"
+let cbool = gen_constant Structures.init_modules "bool"
+let ctrue = gen_constant Structures.init_modules "true"
+let cfalse = gen_constant Structures.init_modules "false"
+let candb = gen_constant Structures.init_modules "andb"
+let corb = gen_constant Structures.init_modules "orb"
+let cxorb = gen_constant Structures.init_modules "xorb"
+let cnegb = gen_constant Structures.init_modules "negb"
+let cimplb = gen_constant Structures.init_modules "implb"
 let ceqb = gen_constant  bool_modules "eqb"
 let cifb = gen_constant bool_modules "ifb"
-let ciff = gen_constant init_modules "iff"
+let ciff = gen_constant Structures.init_modules "iff"
 let creflect = gen_constant bool_modules "reflect"
 
 (* Lists *)
-let clist = gen_constant init_modules "list"
-let cnil = gen_constant init_modules "nil"
-let ccons = gen_constant init_modules "cons"
-let clength = gen_constant init_modules "length"
+let clist = gen_constant Structures.init_modules "list"
+let cnil = gen_constant Structures.init_modules "nil"
+let ccons = gen_constant Structures.init_modules "cons"
+let clength = gen_constant Structures.init_modules "length"
 
 (* Option *)
-let coption = gen_constant init_modules "option"
-let cSome = gen_constant init_modules "Some"
-let cNone = gen_constant init_modules "None"
+let coption = gen_constant Structures.init_modules "option"
+let cSome = gen_constant Structures.init_modules "Some"
+let cNone = gen_constant Structures.init_modules "None"
 
 (* Pairs *)
-let cpair = gen_constant init_modules "pair"
-let cprod = gen_constant init_modules "prod"
+let cpair = gen_constant Structures.init_modules "pair"
+let cprod = gen_constant Structures.init_modules "prod"
 
 (* Dependent pairs *)
-let csigT = gen_constant init_modules "sigT"
-(* let cprojT1 = gen_constant init_modules "projT1" *)
-(* let cprojT2 = gen_constant init_modules "projT2" *)
-(* let cprojT3 = gen_constant init_modules "projT3" *)
+let csigT = gen_constant Structures.init_modules "sigT"
+(* let cprojT1 = gen_constant Structures.init_modules "projT1" *)
+(* let cprojT2 = gen_constant Structures.init_modules "projT2" *)
+(* let cprojT3 = gen_constant Structures.init_modules "projT3" *)
 
-(* let csigT2 = gen_constant init_modules "sigT2" *)
-(* let csigT_of_sigT2 = gen_constant init_modules "sigT_of_sigT2" *)
+(* let csigT2 = gen_constant Structures.init_modules "sigT2" *)
+(* let csigT_of_sigT2 = gen_constant Structures.init_modules "sigT_of_sigT2" *)
 
 (* Logical Operators *)
-let cnot = gen_constant init_modules "not"
-let ceq = gen_constant init_modules "eq"
-let crefl_equal = gen_constant init_modules "eq_refl"
-let cconj = gen_constant init_modules "conj"
-let cand = gen_constant init_modules "and"
+let cnot = gen_constant Structures.init_modules "not"
+let ceq = gen_constant Structures.init_modules "eq"
+let crefl_equal = gen_constant Structures.init_modules "eq_refl"
+let cconj = gen_constant Structures.init_modules "conj"
+let cand = gen_constant Structures.init_modules "and"
 
 (* Bit vectors *)
 let bv_modules = [["SMTCoq";"bva";"BVList";"BITVECTOR_LIST"]]
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 12aef5a..044ff4c 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -80,11 +80,11 @@ module type FORM =
     val clear : reify -> unit
     val get : ?declare:bool -> reify -> pform -> t
 
-    (** Give a coq term, build the corresponding formula *)
+    (** Given a coq term, build the corresponding formula *)
     val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t
 
     val hash_hform : (hatom -> hatom) -> reify -> t -> t
-    (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
+    (* Flattening of [Fand] and [For], removing of [Fnot2]  *)
     val flatten : reify -> t -> t
 
     (** Turn n-ary [Fand] and [For] into their right-associative
@@ -100,10 +100,10 @@ module type FORM =
     val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
     val interp_tbl : reify -> Structures.constr * Structures.constr
     val nvars : reify -> int
-    (** Producing a Coq term corresponding to the interpretation
-          of a formula *)
-    (** [interp_atom] map [hatom] to coq term, it is better if it produce
-          shared terms. *)
+    (* Producing a Coq term corresponding to the interpretation
+       of a formula *)
+    (* [interp_atom] map [hatom] to coq term, it is better if it produce
+       shared terms. *)
     val interp_to_coq :
       (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
       t -> Structures.constr
@@ -589,9 +589,9 @@ module Make (Atom:ATOM) =
       (mkInt i, Structures.mkArray (Lazy.force cform, t))
 
     let nvars reify = reify.count
-    (** Producing a Coq term corresponding to the interpretation of a formula *)
-    (** [interp_atom] map [Atom.t] to coq term, it is better if it produce
-	shared terms. *)
+    (* Producing a Coq term corresponding to the interpretation of a formula *)
+    (* [interp_atom] map [Atom.t] to coq term, it is better if it produce
+       shared terms. *)
     let interp_to_coq interp_atom form_tbl f =
       let rec interp_form f =
 	let l = to_lit f in
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli
index ad7d2ca..fead657 100644
--- a/src/trace/smtForm.mli
+++ b/src/trace/smtForm.mli
@@ -97,10 +97,10 @@ module type FORM =
       val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
       val interp_tbl : reify -> Structures.constr * Structures.constr
       val nvars : reify -> int
-      (** Producing a Coq term corresponding to the interpretation
-          of a formula *)
-      (** [interp_atom] map [hatom] to coq term, it is better if it produce
-          shared terms. *)
+      (* Producing a Coq term corresponding to the interpretation
+         of a formula *)
+      (* [interp_atom] map [hatom] to coq term, it is better if it produce
+         shared terms. *)
       val interp_to_coq :
 	  (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t ->
 	    t -> Structures.constr
diff --git a/src/trace/smtMisc.ml b/src/trace/smtMisc.ml
index 92f0f09..607ebe7 100644
--- a/src/trace/smtMisc.ml
+++ b/src/trace/smtMisc.ml
@@ -46,7 +46,7 @@ type logic_item =
 
 module SL = Set.Make (struct
     type t = logic_item
-    let compare = Pervasives.compare
+    let compare = Stdlib.compare
   end)
 
 type logic = SL.t
diff --git a/src/trace/smtTrace.ml b/src/trace/smtTrace.ml
index f397826..ef017a7 100644
--- a/src/trace/smtTrace.ml
+++ b/src/trace/smtTrace.ml
@@ -159,7 +159,7 @@ let order_roots init_index first =
                   r := n
     | _ -> failwith "root value has unexpected form" end
   done;
-  let _, lr = List.sort (fun (i1, _) (i2, _) -> Pervasives.compare i1 i2) !acc
+  let _, lr = List.sort (fun (i1, _) (i2, _) -> Stdlib.compare i1 i2) !acc
              |> List.split in
   let link_to c1 c2 =
     let curr_id = c2.id -1 in
@@ -476,7 +476,7 @@ let to_coq to_lit interp (cstep,
            let concl' = out_cl [concl] in
            let app_name = Structures.mkId ("app" ^ (string_of_int (Hashtbl.hash concl))) in
            let app_var = Structures.mkVar app_name in
-           let app_ty = Term.mkArrow clemma (interp ([], [concl])) in
+           let app_ty = Structures.mkArrow clemma (interp ([], [concl])) in
            cuts := (app_name, app_ty)::!cuts;
            mklApp cForallInst [|out_c c; clemma; cplemma; concl'; app_var|]
 	end
diff --git a/src/versions/standard/_CoqProject b/src/versions/standard/_CoqProject
index 396a5ba..d7cffca 100644
--- a/src/versions/standard/_CoqProject
+++ b/src/versions/standard/_CoqProject
@@ -38,9 +38,6 @@ 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
deleted file mode 100644
index d957110..0000000
--- a/src/versions/standard/coq_micromega_full.ml
+++ /dev/null
@@ -1,2215 +0,0 @@
-(*** 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
deleted file mode 100644
index efa2e4d..0000000
--- a/src/versions/standard/mutils_full.ml
+++ /dev/null
@@ -1,358 +0,0 @@
-(*** 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
deleted file mode 100644
index d506485..0000000
--- a/src/versions/standard/mutils_full.mli
+++ /dev/null
@@ -1,77 +0,0 @@
-(*** 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 81ac24b..f210db1 100644
--- a/src/versions/standard/smtcoq_plugin_standard.mlpack
+++ b/src/versions/standard/smtcoq_plugin_standard.mlpack
@@ -1,5 +1,3 @@
-Mutils_full
-Coq_micromega_full
 Structures
 
 SmtMisc
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index d7e7f96..becab90 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -41,9 +41,10 @@ let destRel = Constr.destRel
 let lift = Vars.lift
 let mkApp = Constr.mkApp
 let decompose_app = Constr.decompose_app
-let mkLambda = Constr.mkLambda
-let mkProd = Constr.mkProd
-let mkLetIn = Constr.mkLetIn
+let mkLambda (n, t, c) = Constr.mkLambda (Context.make_annot n Sorts.Relevant, t, c)
+let mkProd (n, t, c) = Constr.mkProd (Context.make_annot n Sorts.Relevant, t, c)
+let mkLetIn (n, c1, t, c2) = Constr.mkLetIn (Context.make_annot n Sorts.Relevant, c1, t, c2)
+let mkArrow a b = Term.mkArrow a Sorts.Relevant b
 
 let pr_constr_env env = Printer.pr_constr_env env Evd.empty
 let pr_constr = pr_constr_env Environ.empty_env
@@ -58,7 +59,7 @@ let mkUConst : Constr.t -> Safe_typing.private_constants Entries.definition_entr
     const_entry_secctx      = None;
     const_entry_feedback    = None;
     const_entry_type        = Some (EConstr.Unsafe.to_constr ty); (* Cannot contain evars since it comes from a Constr.t *)
-    const_entry_universes   = Evd.const_univ_entry ~poly:false evd;
+    const_entry_universes   = Evd.univ_entry ~poly:false evd;
     const_entry_opaque      = false;
     const_entry_inline_code = false }
 
@@ -71,20 +72,20 @@ let mkTConst c noc ty =
     const_entry_secctx      = None;
     const_entry_feedback    = None;
     const_entry_type        = Some ty;
-    const_entry_universes   = Evd.const_univ_entry ~poly:false evd;
+    const_entry_universes   = Evd.univ_entry ~poly:false evd;
     const_entry_opaque      = false;
     const_entry_inline_code = false }
 
 (* 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) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make t) in
+  let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Constr.mkSet, Entries.Monomorphic_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) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in
+  let _ = ComAssumption.declare_assumption ~pstate:None false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Evd.univ_entry ~poly:false evd) UnivNames.empty_binders [] false Declaremods.NoInline (CAst.make v) in
   Constr.mkVar v
 
 let declare_constant n c =
@@ -103,8 +104,11 @@ let econstr_of_constr = EConstr.of_constr
 
 
 (* Modules *)
-let gen_constant_in_modules s m n = UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n
+let gen_constant_in_modules s m n =
+  (* UnivGen.constr_of_monomorphic_global will crash on universe polymorphic constants *)
+  UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules s m n
 let gen_constant modules constant = lazy (gen_constant_in_modules "SMT" modules constant)
+let init_modules = Coqlib.init_modules
 
 
 (* Int63 *)
@@ -166,13 +170,13 @@ let mkTrace step_to_coq next _ clist cnil ccons cpair size step def_step r =
 
 (* Micromega *)
 module Micromega_plugin_Micromega = Micromega_plugin.Micromega
-module Micromega_plugin_Mutils = Mutils_full
+module Micromega_plugin_Mutils = Micromega_plugin.Mutils
 module Micromega_plugin_Certificate = Micromega_plugin.Certificate
-module Micromega_plugin_Coq_micromega = Coq_micromega_full
+module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega
 
 let micromega_coq_proofTerm =
   (* Cannot contain evars *)
-  lazy (EConstr.Unsafe.to_constr (Lazy.force (Micromega_plugin_Coq_micromega.M.coq_proofTerm)))
+  lazy (gen_constant_in_modules "ZMicromega" [["Coq"; "micromega";"ZMicromega"]] "ZArithProof")
 
 let micromega_dump_proof_term p =
   (* Cannot contain evars *)
@@ -188,7 +192,7 @@ let assert_before n c = Tactics.assert_before n (EConstr.of_constr c)
 let vm_cast_no_check c = Tactics.vm_cast_no_check (EConstr.of_constr c)
 
 let mk_tactic tac =
-  Proofview.Goal.nf_enter (fun gl ->
+  Proofview.Goal.enter (fun gl ->
     let env = Proofview.Goal.env gl in
     let sigma = Tacmach.New.project gl in
     let t = Proofview.Goal.concl gl in
@@ -222,7 +226,8 @@ let constrextern_extern_constr c =
   Constrextern.extern_constr false env (Evd.from_env env) (EConstr.of_constr c)
 
 let get_rel_dec_name = function
-  | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) -> n
+  | Context.Rel.Declaration.LocalAssum (n, _) | Context.Rel.Declaration.LocalDef (n, _, _) ->
+     Context.binder_name n
 
 let retyping_get_type_of env sigma c =
   (* Cannot contain evars since it comes from a Constr.t *)
diff --git a/src/versions/standard/structures.mli b/src/versions/standard/structures.mli
index cde4f4f..1c4443e 100644
--- a/src/versions/standard/structures.mli
+++ b/src/versions/standard/structures.mli
@@ -38,6 +38,7 @@ val decompose_app : constr -> constr * constr list
 val mkLambda : name * types * constr -> constr
 val mkProd : name * types * types -> types
 val mkLetIn : name * constr * types * constr -> constr
+val mkArrow : types -> types -> constr
 
 val pr_constr_env : Environ.env -> constr -> Pp.t
 val pr_constr : constr -> Pp.t
@@ -60,6 +61,7 @@ val econstr_of_constr : constr -> econstr
 
 (* Modules *)
 val gen_constant : string list list -> string -> constr lazy_t
+val init_modules : string list list
 
 
 (* Int63 *)
@@ -88,9 +90,9 @@ val mkTrace :
 
 (* Micromega *)
 module Micromega_plugin_Micromega = Micromega_plugin.Micromega
-module Micromega_plugin_Mutils = Mutils_full
+module Micromega_plugin_Mutils = Micromega_plugin.Mutils
 module Micromega_plugin_Certificate = Micromega_plugin.Certificate
-module Micromega_plugin_Coq_micromega = Coq_micromega_full
+module Micromega_plugin_Coq_micromega = Micromega_plugin.Coq_micromega
 
 val micromega_coq_proofTerm : constr lazy_t
 val micromega_dump_proof_term : Micromega_plugin_Micromega.zArithProof -> constr
diff --git a/src/zchaff/zchaff.ml b/src/zchaff/zchaff.ml
index 71b28a8..225a90b 100644
--- a/src/zchaff/zchaff.ml
+++ b/src/zchaff/zchaff.ml
@@ -222,7 +222,7 @@ let theorems interp name fdimacs ftrace =
    mklApp cCertif [|mkInt (max_id + 1);tres;mkInt (get_pos confl)|] in
 
   let theorem_concl = mklApp cnot [|mklApp cis_true [|interp d first last|] |] in
-  let vtype = Term.mkArrow (Lazy.force cint) (Lazy.force cbool) in
+  let vtype = Structures.mkArrow (Lazy.force cint) (Lazy.force cbool) in
   let theorem_type =
     Structures.mkProd (Structures.mkName "v", vtype, theorem_concl) in
   let theorem_proof_cast =