diff --git a/dev/ci/scripts/ci-stdlib.sh b/dev/ci/scripts/ci-stdlib.sh
index f6c9d66f9f35..f4fadc17b2db 100644
--- a/dev/ci/scripts/ci-stdlib.sh
+++ b/dev/ci/scripts/ci-stdlib.sh
@@ -10,6 +10,6 @@ git_download stdlib
 if [ "$DOWNLOAD_ONLY" ]; then exit 0; fi
 
 ( cd "${CI_BUILD_DIR}/stdlib"
-  dev/with-rocq-wrap.sh dune build --root . --only-packages=rocq-stdlib @install
+  dev/with-rocq-wrap.sh dune build --root . --profile release --only-packages=rocq-stdlib @install
   dev/with-rocq-wrap.sh dune install --root . rocq-stdlib --prefix="$CI_INSTALL_DIR"
 )
diff --git a/dev/ci/user-overlays/20288-fajb-tify-lra.sh b/dev/ci/user-overlays/20288-fajb-tify-lra.sh
new file mode 100644
index 000000000000..b983ea7bce33
--- /dev/null
+++ b/dev/ci/user-overlays/20288-fajb-tify-lra.sh
@@ -0,0 +1 @@
+overlay stdlib https://github.com/fajb/stdlib rify 20288
diff --git a/doc/corelib/hidden-files b/doc/corelib/hidden-files
index 98e5827a37b1..589e9a9e4eab 100644
--- a/doc/corelib/hidden-files
+++ b/doc/corelib/hidden-files
@@ -39,6 +39,7 @@ theories/micromega/Lra.v
 theories/micromega/MExtraction.v
 theories/micromega/OrderedRing.v
 theories/micromega/Psatz.v
+theories/micromega/MMicromega.v
 theories/micromega/QMicromega.v
 theories/micromega/RMicromega.v
 theories/micromega/Refl.v
diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 4e001526fb8d..30cc1443d5bb 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -153,17 +153,15 @@ For each conjunct :math:`C_i`, the tactic calls an oracle which searches for
 :gdef:`cone expression` that is normalized by the :tacn:`ring` tactic
 (see :ref:`theringandfieldtacticfamilies`) and checked to be :math:`-1`.
 
-`lra`: a decision procedure for linear real and rational arithmetic
+`lra`: a decision procedure for mixed integer linear arithmetic
 -------------------------------------------------------------------
 
 .. tacn:: lra
 
-   This tactic is searching for *linear* refutations. As a result, this tactic explores a subset of the *Cone*
-   defined as
-
-   .. math::
-
-      \mathit{LinCone}(S) =\left\{ \left. \sum_{p \in S} \alpha_p \times p~\right|~\alpha_p \mbox{ are positive constants} \right\}
+   The tactics solves mixed integer arithmetic goals i.e. goals where variables range over either the reals or the integers.
+   In addition to standard linear arithmetic constraints over :g:`R`, the tactic supports the predicate :g:`isZ: R -> Prop`
+   such that :g:`IsZ x` restricts the range of  :g:`x` to be an integer.
+   See  :tacn:`rify` to pre-process the goal.
 
    The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field`
    tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`.
@@ -357,12 +355,57 @@ obtain :math:`-1`. Thus, by Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    See the :ref:`example below <lra_example>` and comments in
    `plugin/micromega/coq_micromega.mli`.
 
-`zify`: pre-processing of arithmetic goals
-------------------------------------------
+`tify`: pre-processing of arithmetic goals (generalise `zify`)
+--------------------------------------------------------------
+
+.. tacn:: tify @qualid
+
+   The tactic :tacn:`tify` :g:`T` injects the goal towards the type
+   :g:`T`. It can be extended with new types and operators by
+   declaring and registering new typeclass instances using the
+   following commands.  The typeclass declarations can be found in the
+   module ``TifyClasses``.
+
+.. cmd:: Add Tify @add_tify @qualid
+
+   .. insertprodn add_tify add_tify
+
+   .. prodn::
+      add_tify ::= {| InjTyp | BinOp | UnOp | CstOp | BinRel | UnOpSpec | BinOpSpec }
+      | {| PropOp | PropBinOp | PropUOp | Saturate }
+
+   Registers an instance of the specified typeclass.
+   The typeclass type (e.g. :g:`BinOp Z.mul` or :g:`BinRel (@eq Z)`) has the additional constraint that
+   the non-implicit argument (here, :g:`Z.mul` or :g:`(@eq Z)`)
+   is either a :n:`@reference` (here, :g:`Z.mul`) or the application of a :n:`@reference` (here, :g:`@eq`) to a sequence of :n:`@one_term`.
+
+   This command supports attributes :attr:`local`, :attr:`export` and :attr:`global`.
+   In sections only :attr:`local` is supported, outside sections the default is :attr:`global`.
+
+.. cmd:: Show Tify @show_tify
+
+   .. insertprodn show_tify show_tify
+
+   .. prodn::
+      show_tify ::= {| InjTyp | BinOp | UnOp | CstOp | BinRel | UnOpSpec | BinOpSpec }
+
+   Prints instances for the specified typeclass.  For instance, :cmd:`Show Tify` ``InjTyp``
+   prints the list of types that supported by :tacn:`tify` e.g.,
+   :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
+
+.. tacn:: tify_elim_let
+          tify_iter_let @ltac_expr
+          tify_iter_specs
+          tify_op @qualid
+          tify_saturate
+
+   For internal use only (it may change without notice).
+
 
 .. tacn:: zify
 
-   This tactic is internally called by :tacn:`lia` to support additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`.
+   This tactic is internally called by :tacn:`lia` and calls tacn:`tify Z` to inject towards :g:`Z`
+   additional types, e.g., :g:`nat`, :g:`positive` and :g:`N`.
    Additional support is provided by the following modules:
 
    + For boolean operators (e.g., :g:`Nat.leb`), require the module :g:`ZifyBool`.
@@ -386,43 +429,28 @@ obtain :math:`-1`. Thus, by Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
      - :g:`Z.euclidean_division_equations_cleanup`, removing impossible hypotheses introduced by the above passes, such as those presupposing :g:`x <> x`
      - :g:`Z.euclidean_division_equations_find_duplicate_quotients`, which heuristically adds equations of the form :g:`q1 = q2 \/ q1 <> q2` when it seems that two quotients might be equal, allowing :g:`nia` to prove more goals, including those relating :g:`Z.quot` and :g:`Z.modulo` to :g:`Z.quot` and :g:`Z.rem`.
 
-   The :tacn:`zify` tactic can be extended with new types and operators by declaring and registering new typeclass instances using the following commands.
-   The typeclass declarations can be found in the module ``ZifyClasses`` and the default instances can be found in the module ``ZifyInst``.
 
-.. cmd:: Add Zify @add_zify @qualid
+.. tacn:: zify_elim_let
+          zify_iter_let @ltac_expr
+          zify_iter_specs
+          zify_op
+          zify_saturate
 
-   .. insertprodn add_zify add_zify
+   For internal use only and deprecated by their tacn:`tify` variants  (it may change without notice).
 
-   .. prodn::
-      add_zify ::= {| InjTyp | BinOp | UnOp | CstOp | BinRel | UnOpSpec | BinOpSpec }
-      | {| PropOp | PropBinOp | PropUOp | Saturate }
+.. cmd:: Add Zify @add_tify @qualid
 
-   Registers an instance of the specified typeclass.
-   The typeclass type (e.g. :g:`BinOp Z.mul` or :g:`BinRel (@eq Z)`) has the additional constraint that
-   the non-implicit argument (here, :g:`Z.mul` or :g:`(@eq Z)`)
-   is either a :n:`@reference` (here, :g:`Z.mul`) or the application of a :n:`@reference` (here, :g:`@eq`) to a sequence of :n:`@one_term`.
+   These commands are deprecated, use :g:`Add Tify` instead.
 
-   This command supports attributes :attr:`local`, :attr:`export` and :attr:`global`.
-   In sections only :attr:`local` is supported, outside sections the default is :attr:`global`.
-
-.. cmd:: Show Zify @show_zify
+.. cmd:: Show Zify @show_tify
 
-   .. insertprodn show_zify show_zify
+   These commands are deprecated, use :g:`Show Tify` instead.
 
-   .. prodn::
-      show_zify ::= {| InjTyp | BinOp | UnOp | CstOp | BinRel | UnOpSpec | BinOpSpec | Spec }
-
-   Prints instances for the specified typeclass.  For instance, :cmd:`Show Zify` ``InjTyp``
-   prints the list of types that supported by :tacn:`zify` i.e.,
-   :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
 
-.. tacn:: zify_elim_let
-          zify_iter_let @ltac_expr
-          zify_iter_specs
-          zify_op
-          zify_saturate
+.. tacn:: rify
 
-   For internal use only (it may change without notice).
+   This tactic (found in module ``Rify``) and defined as tacn:`tify` :g:`R` can used to pre-process goals for tacn:`lra`.
+   In particular, it introduces the predicate :g:`isZ` when injecting variables from :g:`Z` to :g:`R`.
 
 .. _lra_example:
 
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 1312a6acdec4..30ee68a83a30 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -1228,13 +1228,13 @@ printable: [
 | INSERTALL "Print"
 ]
 
-add_zify: [
+add_tify: [
 | [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ]  TAG Micromega
 | [ "PropOp" | "PropBinOp" | "PropUOp" | "Saturate" ]TAG Micromega
 ]
 
-show_zify: [
-| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" | "Spec" ]  TAG Micromega
+show_tify: [
+| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec"  ]  TAG Micromega
 ]
 
 command: [
@@ -1390,8 +1390,19 @@ command: [
 | DELETE "Add" "Zify" "BinOpSpec" reference      (* micromega plugin *)
 | DELETE "Add" "Zify" "UnOpSpec" reference      (* micromega plugin *)
 | DELETE "Add" "Zify" "Saturate" reference      (* micromega plugin *)
-| "Add" "Zify" add_zify reference  TAG Micromega
-
+| "Add" "Zify" add_tify reference  TAG Micromega
+| DELETE "Add" "Tify" "InjTyp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "BinOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "UnOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "CstOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "BinRel" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "PropOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "PropBinOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "PropUOp" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "BinOpSpec" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "UnOpSpec" reference      (* micromega plugin *)
+| DELETE "Add" "Tify" "Saturate" reference      (* micromega plugin *)
+| "Add" "Tify" add_tify reference  TAG Micromega
 | DELETE "Show" "Zify" "InjTyp"      (* micromega plugin *)
 | DELETE "Show" "Zify" "BinOp"      (* micromega plugin *)
 | DELETE "Show" "Zify" "UnOp"      (* micromega plugin *)
@@ -1400,7 +1411,16 @@ command: [
 | DELETE "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
 | DELETE "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
 (* keep this one | "Show" "Zify" "Spec"      (* micromega plugin *)*)
-| "Show" "Zify" show_zify  TAG Micromega
+| "Show" "Zify" show_tify  TAG Micromega
+| DELETE "Show" "Tify" "InjTyp"      (* micromega plugin *)
+| DELETE "Show" "Tify" "BinOp"      (* micromega plugin *)
+| DELETE "Show" "Tify" "UnOp"      (* micromega plugin *)
+| DELETE "Show" "Tify" "CstOp"      (* micromega plugin *)
+| DELETE "Show" "Tify" "BinRel"      (* micromega plugin *)
+| DELETE "Show" "Tify" "UnOpSpec"      (* micromega plugin *)
+| DELETE "Show" "Tify" "BinOpSpec"      (* micromega plugin *)
+(* keep this one | "Show" "Tify" "Spec"      (* micromega plugin *)*)
+| "Show" "Tify" show_tify  TAG Micromega
 | REPLACE "Goal" lconstr
 | WITH "Goal" type
 ]
@@ -1862,6 +1882,8 @@ ltac_defined_tactics: [
 | "tauto"
 | "time_constr" ltac_expr5
 | "zify"
+| "rify"
+| "tify" qualid
 ]
 
 (* todo: need careful review; assume that "[" ... "]" are literals *)
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 82782ef72d38..d9e557eeecd8 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -683,6 +683,17 @@ command: [
 | "Add" "Zify" "BinOpSpec" reference      (* micromega plugin *)
 | "Add" "Zify" "UnOpSpec" reference      (* micromega plugin *)
 | "Add" "Zify" "Saturate" reference      (* micromega plugin *)
+| "Add" "Tify" "InjTyp" reference      (* micromega plugin *)
+| "Add" "Tify" "BinOp" reference      (* micromega plugin *)
+| "Add" "Tify" "UnOp" reference      (* micromega plugin *)
+| "Add" "Tify" "CstOp" reference      (* micromega plugin *)
+| "Add" "Tify" "BinRel" reference      (* micromega plugin *)
+| "Add" "Tify" "PropOp" reference      (* micromega plugin *)
+| "Add" "Tify" "PropBinOp" reference      (* micromega plugin *)
+| "Add" "Tify" "PropUOp" reference      (* micromega plugin *)
+| "Add" "Tify" "BinOpSpec" reference      (* micromega plugin *)
+| "Add" "Tify" "UnOpSpec" reference      (* micromega plugin *)
+| "Add" "Tify" "Saturate" reference      (* micromega plugin *)
 | "Show" "Zify" "InjTyp"      (* micromega plugin *)
 | "Show" "Zify" "BinOp"      (* micromega plugin *)
 | "Show" "Zify" "UnOp"      (* micromega plugin *)
@@ -690,6 +701,13 @@ command: [
 | "Show" "Zify" "BinRel"      (* micromega plugin *)
 | "Show" "Zify" "UnOpSpec"      (* micromega plugin *)
 | "Show" "Zify" "BinOpSpec"      (* micromega plugin *)
+| "Show" "Tify" "InjTyp"      (* micromega plugin *)
+| "Show" "Tify" "BinOp"      (* micromega plugin *)
+| "Show" "Tify" "UnOp"      (* micromega plugin *)
+| "Show" "Tify" "CstOp"      (* micromega plugin *)
+| "Show" "Tify" "BinRel"      (* micromega plugin *)
+| "Show" "Tify" "UnOpSpec"      (* micromega plugin *)
+| "Show" "Tify" "BinOpSpec"      (* micromega plugin *)
 | "Add" "Ring" identref ":" constr OPT ring_mods      (* ring plugin *)
 | "Print" "Rings"      (* ring plugin *)
 | "Add" "Field" identref ":" constr OPT field_mods      (* ring plugin *)
@@ -1962,10 +1980,15 @@ simple_tactic: [
 | "wpsatz_Q" nat_or_var ident constr      (* micromega plugin *)
 | "xpsatz_R" nat_or_var tactic      (* micromega plugin *)
 | "zify_iter_specs"      (* micromega plugin *)
+| "tify_iter_specs"      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
 | "zify_saturate"      (* micromega plugin *)
 | "zify_iter_let" tactic      (* micromega plugin *)
 | "zify_elim_let"      (* micromega plugin *)
+| "tify_op" reference      (* micromega plugin *)
+| "tify_saturate"      (* micromega plugin *)
+| "tify_iter_let" tactic      (* micromega plugin *)
+| "tify_elim_let"      (* micromega plugin *)
 | "nsatz_compute" constr      (* nsatz plugin *)
 | "protect_fv" string "in" ident      (* ring plugin *)
 | "protect_fv" string      (* ring plugin *)
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index 3825b0b3ccb0..e1e90b65adef 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -183,13 +183,13 @@ where: [
 | "after" ident
 ]
 
-add_zify: [
+add_tify: [
 | [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ]      (* Micromega plugin *)
 | [ "PropOp" | "PropBinOp" | "PropUOp" | "Saturate" ]      (* Micromega plugin *)
 ]
 
-show_zify: [
-| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" | "Spec" ]      (* Micromega plugin *)
+show_tify: [
+| [ "InjTyp" | "BinOp" | "UnOp" | "CstOp" | "BinRel" | "UnOpSpec" | "BinOpSpec" ]      (* Micromega plugin *)
 ]
 
 REACHABLE: [
@@ -737,8 +737,10 @@ command: [
 | "Locate" "Term" reference
 | "Locate" "Module" qualid
 | "Info" natural ltac_expr
-| "Add" "Zify" add_zify qualid      (* Micromega plugin *)
-| "Show" "Zify" show_zify      (* Micromega plugin *)
+| "Add" "Zify" add_tify qualid      (* Micromega plugin *)
+| "Show" "Zify" show_tify      (* Micromega plugin *)
+| "Add" "Tify" add_tify qualid      (* Micromega plugin *)
+| "Show" "Tify" show_tify      (* Micromega plugin *)
 | "Locate" "Ltac" qualid
 | "Locate" "Library" qualid
 | "Locate" "File" string
@@ -1608,10 +1610,15 @@ simple_tactic: [
 | "wpsatz_Q" nat_or_var ident one_term      (* micromega plugin *)
 | "xpsatz_R" nat_or_var ltac_expr      (* micromega plugin *)
 | "zify_iter_specs"      (* micromega plugin *)
+| "tify_iter_specs"      (* micromega plugin *)
 | "zify_op"      (* micromega plugin *)
 | "zify_saturate"      (* micromega plugin *)
 | "zify_iter_let" ltac_expr      (* micromega plugin *)
 | "zify_elim_let"      (* micromega plugin *)
+| "tify_op" qualid      (* micromega plugin *)
+| "tify_saturate"      (* micromega plugin *)
+| "tify_iter_let" ltac_expr      (* micromega plugin *)
+| "tify_elim_let"      (* micromega plugin *)
 | "nsatz_compute" one_term      (* nsatz plugin *)
 | "protect_fv" string OPT ( "in" ident )
 | "ring_lookup" ltac_expr0 "[" LIST0 one_term "]" LIST1 one_term      (* ring plugin *)
@@ -1640,6 +1647,8 @@ simple_tactic: [
 | "tauto"
 | "time_constr" ltac_expr
 | "zify"
+| "rify"
+| "tify" qualid
 | "assert_fails" ltac_expr3
 | "assert_succeeds" ltac_expr3
 | "clear" "dependent" ident
diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index f5d0b3b6fb7e..04be0ebd1621 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -106,55 +106,6 @@ let rec_simpl_cone n_spec e =
 
 let simplify_cone n_spec c = fixpoint (rec_simpl_cone n_spec) c
 
-(* The binding with Fourier might be a bit obsolete
-   -- how does it handle equalities ? *)
-
-(* Certificates are elements of the cone such that P = 0  *)
-
-(* To begin with, we search for certificates of the form:
-   a1.p1 + ... an.pn + b1.q1 +... + bn.qn + c = 0
-   where pi >= 0 qi > 0
-   ai >= 0
-   bi >= 0
-   Sum bi + c >= 1
-   This is a linear problem: each monomial is considered as a variable.
-   Hence, we can use fourier.
-
-   The variable c is at index 1
- *)
-
-(* fold_left followed by a rev ! *)
-
-let constrain_variable v l =
-  let coeffs = List.fold_left (fun acc p -> Vect.get v p.coeffs :: acc) [] l in
-  { coeffs =
-      Vect.from_list
-        (Q.of_bigint Z.zero :: Q.of_bigint Z.zero :: List.rev coeffs)
-  ; op = Eq
-  ; cst = Q.of_bigint Z.zero }
-
-let constrain_constant l =
-  let coeffs = List.fold_left (fun acc p -> Q.neg p.cst :: acc) [] l in
-  { coeffs =
-      Vect.from_list (Q.of_bigint Z.zero :: Q.of_bigint Z.one :: List.rev coeffs)
-  ; op = Eq
-  ; cst = Q.of_bigint Z.zero }
-
-let positivity l =
-  let rec xpositivity i l =
-    match l with
-    | [] -> []
-    | c :: l -> (
-      match c.op with
-      | Eq -> xpositivity (i + 1) l
-      | _ ->
-        { coeffs = Vect.update (i + 1) (fun _ -> Q.one) Vect.null
-        ; op = Ge
-        ; cst = Q.zero }
-        :: xpositivity (i + 1) l )
-  in
-  xpositivity 1 l
-
 let cstr_of_poly (p, o) =
   let c, l = Vect.decomp_cst p in
   {coeffs = l; op = o; cst = Q.neg c}
@@ -166,41 +117,9 @@ let make_cstr_system sys =
   in
   List.map map sys
 
-let variables_of_cstr c = Vect.variables c.coeffs
-
 (* If the certificate includes at least one strict inequality,
    the obtained polynomial can also be 0 *)
 
-let build_dual_linear_system l =
-  let variables =
-    List.fold_left
-      (fun acc p -> ISet.union acc (variables_of_cstr p))
-      ISet.empty l
-  in
-  (* For each monomial, compute a constraint *)
-  let s0 =
-    ISet.fold (fun mn res -> constrain_variable mn l :: res) variables []
-  in
-  let c = constrain_constant l in
-  (* I need at least something strictly positive *)
-  let strict =
-    { coeffs =
-        Vect.from_list
-          ( Q.of_bigint Z.zero :: Q.of_bigint Z.one
-          :: List.map
-               (fun c ->
-                 if is_strict c then Q.of_bigint Z.one else Q.of_bigint Z.zero)
-               l )
-    ; op = Ge
-    ; cst = Q.of_bigint Z.one }
-  in
-  (* Add the positivity constraint *)
-  { coeffs = Vect.from_list [Q.of_bigint Z.zero; Q.of_bigint Z.one]
-  ; op = Ge
-  ; cst = Q.of_bigint Z.zero }
-  :: ((strict :: positivity l) @ (c :: s0))
-
-
 let output_cstr_sys o sys =
   List.iter
     (fun (c, wp) ->
@@ -223,35 +142,10 @@ let tr_cstr_sys str f sys =
       output_cstr_sys sys';
   sys'
 
-let dual_raw_certificate l =
-  if debug then begin
-    Printf.printf "dual_raw_certificate\n";
-    List.iter (fun c -> Printf.fprintf stdout "%a\n" output_cstr c) l
-  end;
-  let sys = build_dual_linear_system l in
-  if debug then begin
-    Printf.printf "dual_system\n";
-    List.iter (fun c -> Printf.fprintf stdout "%a\n" output_cstr c) sys
-  end;
-  try
-    match Simplex.find_point sys with
-    | None -> None
-    | Some cert -> (
-      match Vect.choose cert with
-      | None -> failwith "dual_raw_certificate: empty_certificate"
-      | Some _ ->
-        (*Some (rats_to_ints (Vect.to_list (Vect.decr_var 2 (Vect.set 1 Q.zero cert))))*)
-        Some (Vect.normalise (Vect.decr_var 2 (Vect.set 1 Q.zero cert))) )
-    (* should not use rats_to_ints *)
-  with x when CErrors.noncritical x ->
-    if debug then (
-      Printf.printf "dual raw certificate %s" (Printexc.to_string x);
-      flush stdout );
-    None
 
 let simple_linear_prover l =
-  try Simplex.find_unsat_certificate l
-  with Strict ->  dual_raw_certificate l
+  Simplex.find_unsat_certificate l
+
 
 let env_of_list l =
   snd
@@ -304,7 +198,7 @@ exception FoundProof of ProofFormat.prf_rule
     - normalises constraints and generate cuts.
  *)
 
-let check_int_sat (cstr, prf) =
+let check_int_sat isZ (cstr, prf) =
   let {coeffs; op; cst} = cstr in
   match Vect.choose coeffs with
   | None -> if eval_op op Q.zero cst then Tauto else Unsat prf
@@ -312,7 +206,7 @@ let check_int_sat (cstr, prf) =
     let gcdi = Vect.gcd coeffs in
     let gcd = Q.of_bigint gcdi in
     if gcd =/ Q.one then Normalise (cstr, prf)
-    else if Int.equal (Q.sign (Q.mod_ cst gcd)) 0 then begin
+    else if Int.equal (Q.sign (Q.mod_ cst gcd)) 0 || not isZ then begin
       (* We can really normalise *)
       assert (Q.sign gcd >= 1);
       let cstr = {coeffs = Vect.div gcd coeffs; op; cst = cst // gcd} in
@@ -376,6 +270,10 @@ let elim_simple_linear_equality sys0 =
 
 let subst sys = tr_sys "subst" WithProof.subst sys
 
+(*let subst_simple b = tr_sys "subst_simple" (WithProof.subst_simple b)*)
+
+let subst_constant b = tr_sys "subst_constant" (WithProof.subst_constant b)
+
 (** [saturate_linear_equality sys] generate new constraints
     obtained by eliminating linear equalities by pivoting.
     For integers, the obtained constraints are  sound but not complete.
@@ -393,23 +291,31 @@ let elim_redundant sys =
       (fun acc wp ->
         let (_, o), _ = WithProof.repr wp in
         match o with
-        | Gt -> assert false
+        | Gt -> wp :: acc
         | Ge -> wp :: acc
         | Eq -> wp :: WithProof.neg wp :: acc)
       [] sys
   in
+
+  let is_improved_by (q1,o1) (q2,o2) =
+    let cmp = Q.compare q1 q2 in
+    if cmp = 0
+    then
+      match o1 , o2 with
+      | _ , Gt -> true
+      | Ge , Eq -> true
+      |  _ , _ -> false
+    else (cmp > 0) in
+
   let of_list l =
     List.fold_left
       (fun m wp ->
         let (v, o), _ = WithProof.repr wp in
         let q, v' = Vect.decomp_cst v in
         try
-          let q', wp' = VectMap.find v' m in
-          match Q.compare q q' with
-          | 0 -> if o = Eq then VectMap.add v' (q, wp) m else m
-          | 1 -> m
-          | _ -> VectMap.add v' (q, wp) m
-        with Not_found -> VectMap.add v' (q, wp) m)
+          if is_improved_by (fst (VectMap.find v' m)) (q,o)
+          then VectMap.add v' ((q, o), wp) m else m
+        with Not_found -> VectMap.add v' ((q, o), wp) m)
       VectMap.empty l
   in
   let to_list m = VectMap.fold (fun _ (_, wp) sys -> wp :: sys) m [] in
@@ -775,12 +681,12 @@ let extract_coprime_equation psys =
   in
   xextract2 [] psys
 
-let pivot_sys v (cstr, prf) psys =
+let pivot_sys isZ v (cstr, prf) psys =
   let a = Vect.get v cstr.coeffs in
   if a =/ Q.zero then List.rev psys
-  else apply_and_normalise check_int_sat (pivot v (a, cstr, prf)) psys
+  else apply_and_normalise (check_int_sat isZ) (pivot v (a, cstr, prf)) psys
 
-let reduce_coprime psys =
+let reduce_coprime isZ psys =
   let oeq, sys = extract_coprime_equation psys in
   match oeq with
   | None -> None (* Nothing to do *)
@@ -797,12 +703,12 @@ let reduce_coprime psys =
         (ProofFormat.mul_cst_proof l1' p1)
         (ProofFormat.mul_cst_proof l2' p2)
     in
-    Some (pivot_sys v (cstr, prf) ((c1, p1) :: sys))
+    Some (pivot_sys isZ v (cstr, prf) ((c1, p1) :: sys))
 
 (*let pivot_sys v pc sys = tr_cstr_sys "pivot_sys" (pivot_sys v pc) sys*)
 
 (** If there is an equation [eq] of the form 1.x + e = c, do a pivot over x with equation [eq] *)
-let reduce_unary psys =
+let reduce_unary isZ psys =
   let is_unary_equation (cstr, prf) =
     if cstr.op == Eq then
       Vect.find
@@ -815,9 +721,9 @@ let reduce_unary psys =
   | None -> None (* Nothing to do *)
   | Some (v, (cstr, prf)) ->
     let () = assert (cstr.op == Eq) in
-    Some (pivot_sys v (cstr, prf) sys)
+    Some (pivot_sys isZ v (cstr, prf) sys)
 
-let reduce_var_change psys =
+let reduce_var_change isZ psys =
   let rec rel_prime vect =
     match Vect.choose vect with
     | None -> None
@@ -853,58 +759,78 @@ let reduce_var_change psys =
           ; cst = (m */ c.cst) +/ cst }
         , ProofFormat.add_proof (ProofFormat.mul_cst_proof m p) p' )
     in
-    Some (apply_and_normalise check_int_sat pivot_eq sys)
+    Some (apply_and_normalise (check_int_sat isZ) pivot_eq sys)
 
-let reduction_equations psys =
+let reduction_equations isZ psys =
   iterate_until_stable
     (app_funs
-       [reduce_unary; reduce_coprime; reduce_var_change (*; reduce_pivot*)])
+       [reduce_unary isZ; reduce_coprime isZ; reduce_var_change isZ (*; reduce_pivot*)])
     psys
 
-let reduction_equations = tr_cstr_sys "reduction_equations" reduction_equations
+let reduction_equations isZ = tr_cstr_sys "reduction_equations" (reduction_equations isZ)
 
 open ProofFormat
 
-let xlia env sys =
+let xlia isZ env sys =
   let sys = make_cstr_system sys in
-  match reduction_equations sys with
+  match reduction_equations (isZ=None) sys with
   | sys ->
-    let sys = List.map WithProof.of_cstr sys in
-    begin match Simplex.integer_solver sys with
+     if debug then Printf.fprintf stdout "Simplex problem:\n%a\n" output_cstr_sys sys;
+     let sys = List.map WithProof.of_cstr sys in
+     begin match Simplex.integer_solver isZ sys with
     | None -> Unknown
-    | Some prf -> Prf (compile_proof env prf)
+    | Some prf ->
+       begin
+         Prf (compile_proof env prf)
+       end
     end
   | exception FoundProof prf ->
     Prf (compile_proof env (Step (0, prf, Done)))
 
 
-let gen_bench (tac, prover)  prfdepth sys =
-  let res = prover  prfdepth sys in
+let gen_bench (tac, prover)  prfdepth isZ sys =
+  let res = prover  prfdepth isZ sys in
   ( match dump_file () with
   | None -> ()
   | Some file ->
-    let o = open_out (Filename.temp_file ~temp_dir:(Sys.getcwd ()) file ".v") in
-    let _, sys = develop_constraints prfdepth z_spec sys in
-    Printf.fprintf o "Require Import ZArith Lia. Open Scope Z_scope.\n";
-    Printf.fprintf o "Goal %a.\n" (LinPoly.pp_goal "Z") (List.map (fun wp -> fst @@ WithProof.repr wp) sys);
-    begin
-      match res with
-      | Unknown | Model _ ->
-        Printf.fprintf o "Proof.\n intros. Fail %s.\nAbort.\n" tac
-      | Prf res -> Printf.fprintf o "Proof.\n intros. %s.\nQed.\n" tac
-    end;
+     let fn = (Filename.temp_file ~temp_dir:(Sys.getcwd ()) file ".v") in
+     let o = open_out fn in
+     let _, sys = develop_constraints prfdepth z_spec sys in
+     let (typ,import) =
+       if isZ = None
+       then ("Z","Require Import ZArith Lia. Open Scope Z_scope.\n")
+       else ("R","Require Import Reals Lra. Open Scope R_scope.\n") in
+     output_string o import;
+     Printf.fprintf o "Goal %a.\n" (LinPoly.pp_goal typ) (List.map (fun wp -> fst @@ WithProof.repr wp) sys);
+     begin
+       match res with
+       | Unknown | Model _ ->
+          Printf.fprintf o "Proof.\n intros. Fail %s.\nAbort.\n" tac
+       | Prf res -> Printf.fprintf o "Proof.\n intros. %s.\nQed.\n" tac
+     end;
+    Printf.fprintf stdout "Benchmark saved in %s\n" fn;
     flush o; close_out o );
   res
 
-let normalise sys =
+
+let normalise isZ sys =
+  let cp =
+    match isZ with
+    | None -> WithProof.cutting_plane
+    | Some s ->
+       WithProof.cutting_plane_isz isZ in
   List.fold_left
     (fun acc s ->
-      match WithProof.cutting_plane s with
-      | None -> s :: acc
-      | Some s' -> s' :: acc)
+         match cp s with
+         | None -> s :: acc
+         | Some s' -> s' :: acc)
     [] sys
 
-let normalise = tr_sys "normalise" normalise
+
+
+
+
+let normalise isZ = tr_sys "normalise" (normalise isZ)
 
 
 (** [fourier_small] performs some variable elimination and keeps the cutting planes.
@@ -916,19 +842,22 @@ let normalise = tr_sys "normalise" normalise
     When there are several variables, we hope to eliminate all the variables.
     A necessary condition is to take the variable with the smallest coefficient *)
 
-let try_pivot qx wp wp' =
-  match WithProof.simple_pivot qx wp wp' with
-  | None -> None
-  | Some wp2 ->
-    match WithProof.cutting_plane wp2 with
-    | Some wp2 -> Some wp2
+let try_pivot isZ qx wp wp' =
+  if isZ = None
+  then
+    match WithProof.simple_pivot qx wp wp' with
     | None -> None
+    | Some wp2 ->
+       match WithProof.cutting_plane wp2 with
+       | Some wp2 -> Some wp2
+       | None -> None
+  else None
 
-let fourier_small (sys : WithProof.t list) =
+let fourier_small isZ (sys : WithProof.t list) =
   let module WPset = Set.Make(WithProof) in
   let gen_pivot acc qx wp l =
     let fold acc wp' =
-      match try_pivot qx wp wp' with
+      match try_pivot isZ qx wp wp' with
       | None -> acc
       | Some wp2 -> WPset.add wp2 acc
     in
@@ -944,7 +873,7 @@ let fourier_small (sys : WithProof.t list) =
   let res = all_pivots WPset.empty sys in
   WPset.elements res
 
-let fourier_small = tr_sys "fourier_small" fourier_small
+let fourier_small isZ = tr_sys "fourier_small" (fourier_small isZ)
 
 (** [propagate_bounds sys] generate new constraints by exploiting bounds.
     A bound is a constraint of the form c + a.x >= 0
@@ -956,11 +885,12 @@ let rev_concat l =
   in
   conc [] l
 
-let pre_process sys =
-  let sys = normalise sys in
+let pre_process isZ sys =
+  let sys = normalise isZ sys in
   let bnd1 = bound_monomials sys in
-  let sys1 = normalise (subst (List.rev_append sys bnd1)) in
-  let pbnd1 = fourier_small sys1 in
+  let sys = subst_constant (isZ = None) sys in
+  let sys1 = normalise isZ (subst (List.rev_append sys bnd1)) in
+  let pbnd1 = fourier_small isZ sys1 in
   let sys2 = elim_redundant (List.rev_append pbnd1 sys1) in
   let bnd2 = bound_monomials sys2 in
   (* Should iterate ? *)
@@ -969,7 +899,7 @@ let pre_process sys =
   in
   sys
 
-let lia (prfdepth : int) sys =
+let lia (prfdepth : int) isZ sys =
   let env, sys = develop_constraints prfdepth z_spec sys in
   if debug then begin
     Printf.fprintf stdout "Input problem\n";
@@ -983,10 +913,10 @@ let lia (prfdepth : int) sys =
           p)
       sys
   end;
-  let sys = pre_process sys in
-  xlia env sys
+  let sys = pre_process isZ sys in
+  xlia isZ env sys
 
-let nlia prfdepth sys =
+let nlia prfdepth isZ sys =
   let env, sys = develop_constraints prfdepth z_spec sys in
   let is_linear = List.for_all (fun wp -> LinPoly.is_linear @@ WithProof.polynomial wp) sys in
   if debug then begin
@@ -994,7 +924,7 @@ let nlia prfdepth sys =
     List.iter (fun s -> Printf.fprintf stdout "%a\n" WithProof.output s) sys
   end;
   if is_linear then
-    xlia env (pre_process sys)
+    xlia isZ env (pre_process isZ sys)
   else
     (*
       let sys1 = elim_every_substitution sys in
@@ -1002,18 +932,18 @@ let nlia prfdepth sys =
       It would only be safe if the variable is linear...
      *)
     let sys1 =
-      normalise
-        (elim_simple_linear_equality (WithProof.subst_constant true sys))
+      normalise isZ
+        (elim_simple_linear_equality (WithProof.subst_constant (isZ = None) sys))
     in
     let bnd1 = bound_monomials sys1 in
     let sys2 = saturate_by_linear_equalities sys1 in
     let sys3 = nlinear_preprocess (rev_concat [bnd1; sys1; sys2]) in
-    xlia env sys3
+    xlia isZ env sys3
 
 (* For regression testing, if bench = true generate a Rocq goal *)
 
-let lia  prfdepth sys = gen_bench ("lia", lia)  prfdepth sys
-let nlia  prfdepth sys = gen_bench ("nia", nlia)  prfdepth sys
+let lia  ?(isZ=None) prfdepth sys = gen_bench ((if isZ=None then "lia" else "lra"), lia)  prfdepth isZ sys
+let nlia ?(isZ=None) prfdepth sys = gen_bench ((if isZ=None then "nia" else "nra"), nlia)  prfdepth isZ sys
 
 (* Local Variables: *)
 (* coding: utf-8 *)
diff --git a/plugins/micromega/certificate.mli b/plugins/micromega/certificate.mli
index 320596062139..40873d56f774 100644
--- a/plugins/micromega/certificate.mli
+++ b/plugins/micromega/certificate.mli
@@ -8,6 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Mutils
 module Mc = Micromega
 
 type ('prf, 'model) res = Prf of 'prf | Model of 'model | Unknown
@@ -21,11 +22,11 @@ val q_cert_of_pos : Sos_types.positivstellensatz -> Mc.q Mc.psatz
 val z_cert_of_pos : Sos_types.positivstellensatz -> Mc.z Mc.psatz
 
 (** [lia depth sys] generates an unsat proof for the linear constraints in [sys]. *)
-val lia : int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres
+val lia : ?isZ:ISet.t option -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres
 
 (** [nlia depth sys] generates an unsat proof for the non-linear constraints in [sys].
     The solver is incomplete -- the problem is undecidable *)
-val nlia : int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres
+val nlia : ?isZ:ISet.t option -> int ->  (Mc.z Mc.pExpr * Mc.op1) list -> zres
 
 (** [linear_prover_with_cert depth sys] generates an unsat proof for the linear constraints in [sys].
     Over the rationals, the solver is complete. *)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 5558a7e7397e..7922fc16663b 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -81,6 +81,18 @@ let { Goptions.get = use_nia_cache } =
     ~value:true
     ()
 
+let { Goptions.get = use_lra_cache } =
+  declare_bool_option_and_ref
+    ~key:["Lra"; "Cache"]
+    ~value:true
+    ()
+
+let { Goptions.get = use_lqa_cache } =
+  declare_bool_option_and_ref
+    ~key:["Lqa"; "Cache"]
+    ~value:true
+    ()
+
 let { Goptions.get = use_nra_cache } =
   declare_bool_option_and_ref
     ~key:["Nra"; "Cache"]
@@ -110,21 +122,20 @@ module Mc = Micromega
   * parametrized by 'cst, which is used as the type of constants.
   *)
 
-type 'cst atom = 'cst Mc.formula
+type 'f formula =
+  ('f, EConstr.constr, tag * EConstr.constr, Names.Id.t) Mc.gFormula
 
-type 'cst formula =
-  ('cst atom, EConstr.constr, tag * EConstr.constr, Names.Id.t) Mc.gFormula
+type 'f clause = ('f, tag * EConstr.constr) Mc.clause
+type 'f cnf = ('f, tag * EConstr.constr) Mc.cnf
 
-type 'cst clause = ('cst Mc.nFormula, tag * EConstr.constr) Mc.clause
-type 'cst cnf = ('cst Mc.nFormula, tag * EConstr.constr) Mc.cnf
+let kind_is_prop = function Mc.IsProp -> true | Mc.IsBool -> false
 
-let pp_kind o = function
+(*
+  let pp_kind o = function
   | Mc.IsProp -> output_string o "Prop"
   | Mc.IsBool -> output_string o "bool"
 
-let kind_is_prop = function Mc.IsProp -> true | Mc.IsBool -> false
-
-let rec pp_formula o (f : 'cst formula) =
+  let rec pp_formula o (f : 'cst formula) =
   Mc.(
     match f with
     | TT k -> output_string o (if kind_is_prop k then "True" else "true")
@@ -142,6 +153,7 @@ let rec pp_formula o (f : 'cst formula) =
     | IFF (_, f1, f2) ->
       Printf.fprintf o "IFF(%a,%a)" pp_formula f1 pp_formula f2
     | EQ (f1, f2) -> Printf.fprintf o "EQ(%a,%a)" pp_formula f1 pp_formula f2)
+ *)
 
 (**
   * Given a set of integers s=\{i0,...,iN\} and a list m, return the list of
@@ -321,6 +333,10 @@ let rocq_eKind = lazy (constr_of_ref "micromega.eKind")
 let rocq_QWitness = lazy (constr_of_ref "micromega.QWitness.type")
 let rocq_Build = lazy (constr_of_ref "micromega.Formula.Build_Formula")
 let rocq_Cstr = lazy (constr_of_ref "micromega.Formula.type")
+let rocq_eFormula = lazy (constr_of_ref "micromega.eFormula.type")
+let rocq_IsZ = lazy (constr_of_ref "micromega.eFormula.IsZ")
+let rocq_IsF = lazy (constr_of_ref "micromega.eFormula.IsF")
+let rocq_isZ = lazy (constr_of_ref "micromega.isZ")
 
 (**
     * Parsing and dumping : transformation functions between Caml and Rocq
@@ -545,17 +561,19 @@ let dump_pol typ dump_c e =
   dump_pol e
 
 
-(* let pp_clause pp_c o (f: 'cst clause) =
-   List.iter (fun ((p,_),(t,_)) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c)  p Tag.pp t) f *)
+(*let pp_clause pp_c o (f: 'cst clause) =
+  List.iter (fun ((p,_),(t,_)) -> Printf.fprintf o "(%a @%a)" (pp_pol pp_c)  p Tag.pp t) f
 
 let pp_clause_tag o (f : 'cst clause) =
   List.iter (fun ((p, _), (t, _)) -> Printf.fprintf o "(_ @%a)" Tag.pp t) f
 
-(* let pp_cnf pp_c o (f:'cst cnf) =
-   List.iter (fun l -> Printf.fprintf o "[%a]" (pp_clause pp_c) l) f *)
+ let pp_cnf pp_c o (f:'cst cnf) =
+   List.iter (fun l -> Printf.fprintf o "[%a]" (pp_clause pp_c) l) f
 
 let pp_cnf_tag o (f : 'cst cnf) =
   List.iter (fun l -> Printf.fprintf o "[%a]" pp_clause_tag l) f
+ *)
+
 
 let dump_psatz typ dump_z e =
   let z = Lazy.force typ in
@@ -614,6 +632,13 @@ let dump_cstr typ dump_constant {Mc.flhs = e1; Mc.fop = o; Mc.frhs = e2} =
        ; dump_op o
        ; dump_expr typ dump_constant e2 |] )
 
+let dump_bool b = Lazy.force (if b then rocq_true else rocq_false)
+
+let parse_bool sigma b =
+  if EConstr.eq_constr sigma b (Lazy.force rocq_true) then true else false
+
+
+
 let assoc_const sigma x l =
   try
     snd (List.find (fun (x', y) -> EConstr.eq_constr sigma x (Lazy.force x')) l)
@@ -911,6 +936,39 @@ let rconstant (genv, sigma) term =
     flush stdout );
   res
 
+
+let parse_eformula parse_f (k:Mc.kind) (env:Env.t) cstr (genv,sigma) =
+  let is c c' = EConstr.eq_constr sigma c (Lazy.force c') in
+  match EConstr.kind sigma cstr with
+  | App(c, [|x|]) when is c rocq_isZ -> (* we are in Prop *)
+     let (env,x) = Env.compute_rank_add env x Mc.IsBool in
+     Mc.IsZ(true, x),env
+  | _  -> parse_f k env cstr (genv,sigma)
+
+let dump_eformula typ_f dump_f e =
+  match e with
+  | Mc.IsZ(b,x) -> EConstr.mkApp(Lazy.force rocq_IsZ, [| typ_f ; dump_bool b; dump_positive x|])
+  | Mc.IsF f    -> EConstr.mkApp(Lazy.force rocq_IsF, [| typ_f ; dump_f f|])
+
+
+
+
+let undump_eformula undump_atom  sigma f =
+  let is c c' = EConstr.eq_constr sigma c (Lazy.force c') in
+  match EConstr.kind sigma f with
+  | App (c, [|_;b;x|]) when is c rocq_IsZ -> Mc.IsZ (parse_bool sigma b,undump_var sigma x)
+  | App (c, [|_;f|]) when is c rocq_IsF   -> Mc.IsF (undump_atom sigma f)
+  | _ -> raise ParseError
+
+let pp_eformula pp_form o e =
+  match e with
+  | Mc.IsZ(b,x) -> Printf.fprintf o "IsZ(%b,%a)" b pp_positive x
+  | Mc.IsF f    -> Printf.fprintf o "IsF %a" pp_form f
+
+let undump_rconstant sigma term =
+  rconstant (Global.env (), sigma) term
+
+
 let parse_qexpr gl =
   parse_expr gl qconstant
     (fun expr x ->
@@ -950,6 +1008,17 @@ 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
 
+(* [parse_rarith_ext] constructs [eFormula (formula rcst)]
+   i.e. in addition to formula, it also parses the [isZ] predicate. *)
+
+let parse_rarith_ext (k:Mc.kind) (env:Env.t) (cstr: Evd.econstr) (genv,sigma) =
+  let parse_f k env c (genv,sigma)  =
+    let (f,e) = (parse_rarith k env cstr (genv,sigma)) in
+    Mc.IsF f, e in
+  parse_eformula parse_f k env cstr (genv,sigma)
+
+
+
 (* generic parsing of arithmetic expressions *)
 
 let mkAND b f1 f2 = Mc.AND (b, f1, f2)
@@ -1057,8 +1126,6 @@ let parse_formula (genv, sigma) parse_atom env tg term =
   in
   xparse_formula prop_op Mc.IsProp env tg (*Reductionops.whd_zeta*) term
 
-(*  let dump_bool b = Lazy.force (if b then rocq_true else rocq_false)*)
-
 let undump_kind sigma k =
   if EConstr.eq_constr sigma k (Lazy.force rocq_IsProp) then Mc.IsProp
   else Mc.IsBool
@@ -1135,17 +1202,23 @@ let prop_env_of_formula gl form =
     in
     doit (Env.empty gl) form)
 
-let var_env_of_formula form =
-  let rec vars_of_expr = function
+
+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 vars_of_cstr {Mc.flhs; Mc.fop; Mc.frhs} =
+  ISet.union (vars_of_expr flhs) (vars_of_expr frhs)
+
+let vars_of_eformula = function
+  | Mc.IsZ(_,x) -> ISet.singleton (CoqToCaml.positive x)
+  | Mc.IsF f    -> vars_of_cstr f
+
+
+let vars_of_formula vars_of_atom form =
   Mc.(
     let rec doit = function
       | TT _ | FF _ | X _ -> ISet.empty
@@ -1256,16 +1329,65 @@ let eKind = function
   | Mc.IsProp -> EConstr.mkProp
   | Mc.IsBool -> Lazy.force rocq_bool
 
-let make_goal_of_formula gl dexpr form =
+let unreify_expr dexpr varid i  e =
+    let rec unreify_expr = function
+      | Mc.PEX n ->
+        EConstr.mkRel (i + List.assoc (CoqToCaml.positive n) varid)
+      | Mc.PEc z -> dexpr.dump_cst z
+      | Mc.PEadd (e1, e2) ->
+        EConstr.mkApp (dexpr.dump_add, [|unreify_expr e1; unreify_expr e2|])
+      | Mc.PEsub (e1, e2) ->
+        EConstr.mkApp (dexpr.dump_sub, [|unreify_expr e1; unreify_expr e2|])
+      | Mc.PEopp e -> EConstr.mkApp (dexpr.dump_opp, [|unreify_expr e|])
+      | Mc.PEmul (e1, e2) ->
+        EConstr.mkApp (dexpr.dump_mul, [|unreify_expr e1; unreify_expr e2|])
+      | Mc.PEpow (e, n) ->
+        EConstr.mkApp (dexpr.dump_pow, [|unreify_expr e; dexpr.dump_pow_arg n|])
+    in
+    unreify_expr e
+
+let unreify_cstr_prop dexpr varid  i  {Mc.flhs; Mc.fop; Mc.frhs} =
+    let mkop_prop op e1 e2 =
+    try EConstr.mkApp (List.assoc op dexpr.dump_op_prop, [|e1; e2|])
+    with Not_found ->
+      EConstr.mkApp (Lazy.force rocq_eq, [|dexpr.interp_typ; e1; e2|])
+    in
+    mkop_prop fop (unreify_expr dexpr varid  i  flhs)
+      (unreify_expr dexpr varid  i  frhs)
+
+let unreify_cstr_bool dexpr varid  i  {Mc.flhs; Mc.fop; Mc.frhs} =
+  let mkop_bool op e1 e2 =
+    try EConstr.mkApp (List.assoc op dexpr.dump_op_bool, [|e1; e2|])
+    with Not_found ->
+      EConstr.mkApp (Lazy.force rocq_eq, [|dexpr.interp_typ; e1; e2|]) in
+  mkop_bool fop (unreify_expr dexpr varid  i  flhs)
+    (unreify_expr dexpr varid  i  frhs)
+
+let unreify_cstr dexpr k varid i c =
+  match k with
+  | Mc.IsProp -> unreify_cstr_prop dexpr varid i c
+  | Mc.IsBool -> unreify_cstr_bool dexpr varid i c
+
+
+let unreify_eformula dexpr k varid i e =
+  match e with
+  | Mc.IsZ(b,x) -> assert (b = true);
+                   EConstr.mkApp(Lazy.force rocq_isZ, [|
+                                   EConstr.mkRel (i + List.assoc (CoqToCaml.positive x) varid)|])
+  | Mc.IsF f    -> unreify_cstr dexpr k varid i f
+
+
+let make_goal_of_formula gl typ unreify_formula vars_of_atom
+      (form:'f formula) =
   let vars_idx =
-    List.mapi (fun i v -> (v, i + 1)) (ISet.elements (var_env_of_formula form))
+    List.mapi (fun i v -> (v, i + 1)) (ISet.elements (vars_of_formula vars_of_atom 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 gl form in
   let fresh_var str i = Names.Id.of_string (str ^ string_of_int i) in
   let fresh_prop str i = Names.Id.of_string (str ^ string_of_int i) in
   let vars_n =
-    List.map (fun (_, i) -> (fresh_var "__x" i, dexpr.interp_typ)) vars_idx
+    List.map (fun (_, i) -> (fresh_var "__x" i, typ)) vars_idx
   in
   let props_n =
     List.mapi
@@ -1275,39 +1397,6 @@ let make_goal_of_formula gl dexpr form =
   let var_name_pos =
     List.fold_left2 (fun acc (idx, _) (id, _) -> (id, idx) :: acc) [] 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_prop op e1 e2 =
-    try EConstr.mkApp (List.assoc op dexpr.dump_op_prop, [|e1; e2|])
-    with Not_found ->
-      EConstr.mkApp (Lazy.force rocq_eq, [|dexpr.interp_typ; e1; e2|])
-  in
-  let dump_cstr_prop i {Mc.flhs; Mc.fop; Mc.frhs} =
-    mkop_prop fop (dump_expr i flhs) (dump_expr i frhs)
-  in
-  let mkop_bool op e1 e2 =
-    try EConstr.mkApp (List.assoc op dexpr.dump_op_bool, [|e1; e2|])
-    with Not_found ->
-      EConstr.mkApp (Lazy.force rocq_eq, [|dexpr.interp_typ; e1; e2|])
-  in
-  let dump_cstr_bool i {Mc.flhs; Mc.fop; Mc.frhs} =
-    mkop_bool fop (dump_expr i flhs) (dump_expr i frhs)
-  in
   let rec xdump_prop pi xi f =
     match f with
     | Mc.TT _ -> Lazy.force rocq_True
@@ -1330,7 +1419,7 @@ let make_goal_of_formula gl dexpr form =
       EConstr.mkApp
         ( Lazy.force rocq_eq
         , [|Lazy.force rocq_bool; xdump_bool pi xi x; xdump_bool pi xi y|] )
-    | Mc.A (_, x, _) -> dump_cstr_prop xi x
+    | Mc.A (_, x, _) -> unreify_formula Mc.IsProp vars_idx xi x
     | Mc.X (_, t) ->
       let idx = Env.get_rank props t in
       EConstr.mkRel (pi + idx)
@@ -1353,7 +1442,7 @@ let make_goal_of_formula gl dexpr form =
     | Mc.NOT (_, x) ->
       EConstr.mkApp (Lazy.force rocq_negb, [|xdump_bool pi xi x|])
     | Mc.EQ (x, y) -> assert false
-    | Mc.A (_, x, _) -> dump_cstr_bool xi x
+    | Mc.A (_, x, _) -> unreify_formula Mc.IsBool vars_idx xi x
     | Mc.X (_, t) ->
       let idx = Env.get_rank props t in
       EConstr.mkRel (pi + idx)
@@ -1490,41 +1579,69 @@ let parse_goal gl parse_arith (env : Env.t) (hyps:(Names.Id.t * EConstr.types) l
 (**
   * The datastructures that aggregate theory-dependent proof values.
   *)
-type ('synt_c, 'prf) domain_spec =
+type ('formula, 'nformula, '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 *)
+(*  ; (* is the type of the syntactic coeffs - Z , Q , Rcst *)
     dump_coeff : 'synt_c -> EConstr.constr
-  ; undump_coeff : Evd.evar_map -> EConstr.constr -> 'synt_c
+ *)
+  ; undump_formula : Evd.evar_map -> EConstr.t -> 'formula
+  (* A parser for Rocq formulae e.g x + y >= 0 *)
+  ; dump_formula : 'formula -> EConstr.constr
+  (* A printer for (f:'formula) e.g Ge (Add (Var 1) (Var 2)) Zero *)
+  ; vars_of_formula : 'formula -> ISet.t
+  ; unreify_formula :
+      Mc.kind -> (int * int) list -> int -> 'formula -> EConstr.constr
+  (* unreify_formula (undump_formula c) = c *)
   ; proof_typ : EConstr.constr
   ; dump_proof : 'prf -> EConstr.constr
-  ; coeff_eq : 'synt_c -> 'synt_c -> bool }
+  ; nformula_eq : 'nformula -> 'nformula -> bool }
+
+let nformula_eq eq_cst (p1,o1) (p2,o2) =
+    let open Mutils.Hash in
+    eq_pol eq_cst p1 p2 && eq_op1 o1 o2
+
+let eformula_eq eq_cst ef1 ef2 =
+  match ef1 , ef2 with
+  | Mc.IsZ(b1,p1) , Mc.IsZ(b2,p2) -> Bool.equal b1 b2 && Mutils.Hash.eq_positive p1 p2
+  | Mc.IsF f1 , Mc.IsF f2         -> nformula_eq eq_cst f1 f2
+  |   _    , _    -> false
+
 
 let zz_domain_spec =
   lazy
     { typ = Lazy.force rocq_Z
     ; coeff = Lazy.force rocq_Z
-    ; dump_coeff = dump_z
-    ; undump_coeff = parse_z
+(*    ; dump_coeff = dump_z
+    ; undump_coeff = parse_z *)
+    ; undump_formula = undump_cstr parse_z
+    ; vars_of_formula  = vars_of_cstr
+    ; dump_formula = dump_cstr (Lazy.force rocq_Z) dump_z
+    ; unreify_formula = unreify_cstr (Lazy.force dump_zexpr)
     ; proof_typ = Lazy.force rocq_proofTerm
     ; dump_proof = dump_proof_term
-    ; coeff_eq = Mc.Z.eqb }
+    ; nformula_eq = nformula_eq Mc.Z.eqb }
 
 let qq_domain_spec =
   lazy
     { typ = Lazy.force rocq_Q
     ; coeff = Lazy.force rocq_Q
-    ; dump_coeff = dump_q
-    ; undump_coeff = parse_q
+    (*; dump_coeff = dump_q
+    ; undump_coeff = parse_q *)
+    ; vars_of_formula = vars_of_cstr
+    ; undump_formula = undump_cstr parse_q
+    ; dump_formula = dump_cstr (Lazy.force rocq_Q) dump_q
+    ; unreify_formula = unreify_cstr (Lazy.force dump_qexpr)
     ; proof_typ = Lazy.force rocq_QWitness
     ; dump_proof = dump_psatz rocq_Q dump_q
-    ; coeff_eq = Mc.qeq_bool }
+    ; nformula_eq = nformula_eq Mc.qeq_bool }
 
-let max_tag f =
+(*let max_tag f =
   1
   + Tag.to_int
       (Mc.foldA (fun t1 (t2, _) -> Tag.max t1 t2) Mc.IsProp f (Tag.from 0))
+ *)
 
 (** Naive topological sort of constr according to the subterm-ordering *)
 
@@ -1540,7 +1657,7 @@ 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 rocq_Cstr, [|spec.coeff|]) in
-  let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
+  let ff = dump_formula formula_typ spec.dump_formula 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.enter (fun gl ->
@@ -1565,18 +1682,20 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*)
 
 open Certificate
 
-type ('option, 'a, 'prf, 'model) prover =
+type ('option, 'a, 'tag, 'prf, 'model) prover =
   { name : string
   ; (* name of the prover *)
     get_option : unit -> 'option
   ; (* find the options of the prover *)
     prover : 'option * 'a list -> ('prf, 'model) Certificate.res
   ; (* the prover itself *)
-    hyps : 'prf -> ISet.t
+    hyps : ('a * 'tag) list -> '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
+    rebuild_proof_index : ('a * 'tag) list -> ('a * 'tag) list -> int -> int
+  (* given old and new clause, recomputes proof indexes *)
+  ;  pp_prf : out_channel -> 'prf -> unit
   ; (* pretting printing of proof *)
     pp_f : out_channel -> 'a -> unit
         (* pretty printing of the formulas (polynomials)*) }
@@ -1615,25 +1734,24 @@ let witness_list prover l =
   res
  *)
 
+
+
 (**
   * Prune the proof object, according to the 'diff' between two cnf formulas.
   *)
 
-let compact_proofs prover (eq_cst : 'cst -> 'cst -> bool) (cnf_ff : 'cst cnf) res
-    (cnf_ff' : 'cst cnf) =
-  let eq_formula (p1, o1) (p2, o2) =
-    let open Mutils.Hash in
-    eq_pol eq_cst p1 p2 && eq_op1 o1 o2
-  in
-  let compact_proof (old_cl : 'cst clause) prf (new_cl : 'cst clause)
+
+
+
+
+
+
+
+
+let compact_proofs prover (eq_formula: 'f -> 'f -> bool) (cnf_ff : 'f cnf) res
+    (cnf_ff' : 'f cnf) =
+  let compact_proof (old_cl : 'f clause) prf (new_cl : 'f 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
-      CList.assoc_f eq_formula formula new_cl
-    in
     (* if debug then
        begin
          Printf.printf "\ncompact_proof : %a %a %a"
@@ -1643,7 +1761,7 @@ let compact_proofs prover (eq_cst : 'cst -> 'cst -> bool) (cnf_ff : 'cst cnf) re
            flush stdout
        end ; *)
     let res =
-      try prover.compact prf remap
+      try prover.compact prf (prover.rebuild_proof_index old_cl new_cl)
       with x when CErrors.noncritical x -> (
         if debug then
           Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x);
@@ -1658,7 +1776,7 @@ let compact_proofs prover (eq_cst : 'cst -> 'cst -> bool) (cnf_ff : 'cst cnf) re
     end;
     res
   in
-  let is_proof_compatible (hyps, (old_cl : 'cst clause), prf) (new_cl : 'cst clause) =
+  let is_proof_compatible (hyps, (old_cl : 'f clause), prf) (new_cl : 'f clause) =
     let eq (f1, (t1, e1)) (f2, (t2, e2)) =
       Int.equal (Tag.compare t1 t2) 0
       && eq_formula f1 f2
@@ -1668,12 +1786,12 @@ let compact_proofs prover (eq_cst : 'cst -> 'cst -> bool) (cnf_ff : 'cst cnf) re
     is_sublist eq (Lazy.force hyps) new_cl
   in
   let map acc cl prf =
-    let hyps = lazy (selecti (prover.hyps prf) cl) in
+    let hyps = lazy (selecti (prover.hyps cl prf) cl) in
     (hyps, cl, prf) :: acc
   in
   let cnf_res = List.rev (List.fold_left2 map [] cnf_ff res) in
   (* we get pairs clause * proof *)
-  if debug then begin
+ (* if debug then begin
     Printf.printf "CNFRES\n";
     flush stdout;
     Printf.printf "CNFOLD %a\n" pp_cnf_tag cnf_ff;
@@ -1683,7 +1801,7 @@ let compact_proofs prover (eq_cst : 'cst -> 'cst -> bool) (cnf_ff : 'cst cnf) re
         flush stdout)
       cnf_res;
     Printf.printf "CNFNEW %a\n" pp_cnf_tag cnf_ff'
-  end;
+  end; *)
   List.map
     (fun x ->
       let _, o, p =
@@ -1822,14 +1940,16 @@ let rec fold_trace f accu tr =
   | Merge (Push (x, t1), t2) -> fold_trace f (f accu x) (Merge (t1, t2))
   | Merge (Merge (t1, t2), t3) -> fold_trace f accu (Merge (t1, Merge (t2, t3)))
 
-let micromega_tauto ?(abstract=true) pre_process cnf spec prover
-    (polys1 : (Names.Id.t * 'cst formula) list) (polys2 : 'cst formula) =
+type rarith = (Mc.q Mc.formula) Mc.eFormula
+type rformula = rarith formula
+
+let micromega_tauto ?(abstract=true) cnf
+      spec prover
+      polys1 polys2  =
   (* Express the goal as one big implication *)
   let ff, ids = formula_hyps_concl polys1 polys2 in
-  let mt = CamlToCoq.positive (max_tag ff) in
   (* Construction of cnf *)
-  let pre_ff = pre_process mt (ff : 'a formula) in
-  let cnf_ff, cnf_ff_tags = cnf Mc.IsProp pre_ff in
+  let cnf_ff, cnf_ff_tags = cnf Mc.IsProp ff in
   match witness_list prover cnf_ff with
   | Model m -> Model m
   | Unknown -> Unknown
@@ -1845,49 +1965,24 @@ let micromega_tauto ?(abstract=true) pre_process cnf spec prover
                 if debug then Printf.fprintf stdout "T : %i -> %a" i Tag.pp t;
                 (*try*) TagSet.add t s
                 (* with Invalid_argument _ -> s*))
-              (prover.hyps prf) TagSet.empty
+              (prover.hyps cl prf) TagSet.empty
           in
           TagSet.union s tags)
         (fold_trace (fun s (i, _) -> TagSet.add i s) TagSet.empty cnf_ff_tags)
         cnf_ff res
     in
     let ff' = if abstract then abstract_formula deps ff else ff in
-    let pre_ff' = pre_process mt ff' in
-    let cnf_ff', _ = cnf Mc.IsProp pre_ff' in
-    if debug then begin
-      output_string stdout "\n";
-      Printf.printf "TForm    : %a\n" pp_formula ff;
-      flush stdout;
-      Printf.printf "CNF    : %a\n" pp_cnf_tag cnf_ff;
-      flush stdout;
-      Printf.printf "TFormAbs : %a\n" pp_formula ff';
-      flush stdout;
-      Printf.printf "TFormPre : %a\n" pp_formula pre_ff;
-      flush stdout;
-      Printf.printf "TFormPreAbs : %a\n" pp_formula pre_ff';
-      flush stdout;
-      Printf.printf "CNF    : %a\n" pp_cnf_tag cnf_ff';
-      flush stdout
-    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 prover spec.coeff_eq cnf_ff res cnf_ff' in
+    let cnf_ff', _ = cnf Mc.IsProp ff' in
+    let res' = compact_proofs prover spec.nformula_eq cnf_ff res cnf_ff' in
     let ff', res', ids = (ff', res', Mc.ids_of_formula Mc.IsProp ff') in
     let res' = dump_list spec.proof_typ spec.dump_proof res' in
     if show_used_hyps ()
     then Feedback.msg_info Pp.(str "Micromega used hypotheses: "++pr_enum Names.Id.print ids);
     Prf (ids, ff', res')
 
-let micromega_tauto ?abstract pre_process cnf spec prover
-    (polys1 : (Names.Id.t * 'cst formula) list) (polys2 : 'cst formula) =
-  try micromega_tauto ?abstract pre_process cnf spec prover polys1 polys2
+let micromega_tauto ?abstract  cnf spec prover
+      polys1 polys2 =
+  try micromega_tauto ?abstract  cnf spec prover polys1 polys2
   with Not_found ->
     Printexc.print_backtrace stdout;
     flush stdout;
@@ -1910,7 +2005,7 @@ let clear_all_no_check =
           let sigma, ev = Evarutil.new_evar env sigma concl in
           sigma, ev, Some (fst (EConstr.destEvar sigma ev))))
 
-let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac =
+let micromega_gen parse_arith  cnf spec  prover tac =
   Proofview.Goal.enter (fun gl ->
       let sigma = Tacmach.project gl in
       let genv = Tacmach.pf_env gl in
@@ -1924,11 +2019,10 @@ let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac =
         in
         let env = Env.elements env in
         let spec = Lazy.force spec in
-        let dumpexpr = Lazy.force dumpexpr in
         if debug then
           Feedback.msg_debug (Pp.str "Env " ++ Env.pp (genv, sigma) env);
         match
-          micromega_tauto pre_process cnf spec prover hyps concl
+          micromega_tauto cnf spec prover hyps concl
         with
         | Unknown ->
           flush stdout;
@@ -1937,7 +2031,7 @@ let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac =
           Tacticals.tclFAIL (Pp.str " Cannot find witness")
         | Prf (ids, ff', res') ->
           let arith_goal, props, vars, ff_arith =
-            make_goal_of_formula (genv, sigma) dumpexpr ff'
+            make_goal_of_formula (genv, sigma) spec.typ spec.unreify_formula spec.vars_of_formula ff'
           in
           let intro (id, _) = Tactics.introduction id in
           let intro_vars = Tacticals.tclTHENLIST (List.map intro vars) in
@@ -1982,16 +2076,15 @@ Tacticals.tclTHEN
       with
       | CsdpNotFound -> fail_csdp_not_found ())
 
-let micromega_wit_gen pre_process cnf spec prover wit_id ff =
+let micromega_wit_gen  cnf spec prover wit_id ff =
   Proofview.Goal.enter (fun gl ->
       let sigma = Tacmach.project gl in
       try
         let spec = Lazy.force spec in
-        let undump_cstr = undump_cstr spec.undump_coeff in
         let tg = Tag.from 0, Lazy.force rocq_tt in
-        let ff = undump_formula undump_cstr tg sigma ff in
+        let ff = undump_formula spec.undump_formula tg sigma ff in
         match
-          micromega_tauto ~abstract:false pre_process cnf spec prover [] ff
+          micromega_tauto ~abstract:false cnf spec prover [] ff
         with
         | Unknown ->
           flush stdout;
@@ -2010,10 +2103,11 @@ let micromega_order_changer cert env ff =
   let dump_coeff = dump_Rcst in
   let typ = Lazy.force rocq_R in
   let cert_typ =
-    EConstr.mkApp (Lazy.force rocq_list, [|Lazy.force rocq_QWitness|])
+    EConstr.mkApp (Lazy.force rocq_list, [|Lazy.force rocq_proofTerm|])
   in
   let formula_typ = EConstr.mkApp (Lazy.force rocq_Cstr, [|coeff|]) in
-  let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
+  let eformula_typ = EConstr.mkApp (Lazy.force rocq_eFormula,[|formula_typ|]) in
+  let ff = dump_formula eformula_typ (dump_eformula formula_typ (dump_cstr coeff dump_coeff)) ff in
   let vm = dump_varmap typ (vm_of_list env) in
   Proofview.Goal.enter (fun gl ->
     let sigma = Proofview.Goal.sigma gl in
@@ -2024,25 +2118,32 @@ let micromega_order_changer cert env ff =
                  , ff
                  , EConstr.mkApp
                      ( Lazy.force rocq_Formula
-                     , [|formula_typ; Lazy.force rocq_IsProp|] ) )
+                     , [|eformula_typ; Lazy.force rocq_IsProp|] ) )
                ; ("__varmap", vm, EConstr.mkApp (Lazy.force rocq_VarMap, [|typ|]))
                ; ("__wit", cert, cert_typ) ]
                (Tacmach.pf_concl gl))
           (*      Tacticals.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)*)
         ])
 
-let micromega_genr prover tac =
-  let parse_arith = parse_rarith in
-  let spec =
+open Certificate
+
+let rzdomain =
     lazy
       { typ = Lazy.force rocq_R
       ; coeff = Lazy.force rocq_Rcst
-      ; dump_coeff = dump_q
-      ; undump_coeff = parse_q
-      ; proof_typ = Lazy.force rocq_QWitness
-      ; dump_proof = dump_psatz rocq_Q dump_q
-      ; coeff_eq = Mc.qeq_bool }
-  in
+      ; vars_of_formula = vars_of_eformula
+      ; undump_formula = undump_eformula (undump_cstr undump_rconstant)
+      ; dump_formula = dump_eformula (EConstr.mkApp(Lazy.force rocq_Cstr,[| Lazy.force rocq_Rcst|]))
+                         (dump_cstr (Lazy.force rocq_Rcst) dump_Rcst)
+      ; unreify_formula = unreify_eformula (Lazy.force dump_rexpr)
+      ; proof_typ = Lazy.force rocq_proofTerm
+      ; dump_proof = dump_proof_term
+      ; nformula_eq = eformula_eq Mc.qeq_bool
+      }
+
+
+let micromega_genr spec prover tac =
+  let parse_arith = parse_rarith_ext in
   Proofview.Goal.enter (fun gl ->
       let sigma = Tacmach.project gl in
       let genv = Tacmach.pf_env gl in
@@ -2056,24 +2157,22 @@ let micromega_genr prover tac =
         in
         let env = Env.elements env in
         let spec = Lazy.force spec in
-        let hyps' =
+        let (hyps': (Names.Id.t * rformula) list) =
           List.map
             (fun (n, f) ->
               ( n
               , Mc.map_bformula Mc.IsProp
-                  (Micromega.map_Formula Micromega.q_of_Rcst)
+                  (Micromega.map_eFormula Micromega.q_of_Rcst)
                   f ))
             hyps
         in
-        let concl' =
+        let (concl':rformula) =
           Mc.map_bformula Mc.IsProp
-            (Micromega.map_Formula Micromega.q_of_Rcst)
+            (Micromega.map_eFormula Micromega.q_of_Rcst)
             concl
         in
         match
-          micromega_tauto
-            (fun _ x -> x)
-            Mc.cnfQ spec prover hyps' concl'
+          micromega_tauto Mc.cnfR spec prover hyps' concl'
         with
         | Unknown | Model _ ->
           flush stdout;
@@ -2086,7 +2185,7 @@ let micromega_genr prover tac =
           in
           let ff' = abstract_wrt_formula ff' ff in
           let arith_goal, props, vars, ff_arith =
-            make_goal_of_formula (genv, sigma) (Lazy.force dump_rexpr) ff'
+            make_goal_of_formula (genv, sigma) spec.typ spec.unreify_formula spec.vars_of_formula ff'
           in
           let intro (id, _) = Tactics.introduction id in
           let intro_vars = Tacticals.tclTHENLIST (List.map intro vars) in
@@ -2149,28 +2248,27 @@ type provername = string * int option
 
 module MakeCache (T : sig
   type prover_option
-  type coeff
+  type formula
 
   val hash_prover_option : int -> prover_option -> int
-  val hash_coeff : int -> coeff -> int
+  val hash_formula : int -> formula -> int
   val eq_prover_option : prover_option -> prover_option -> bool
-  val eq_coeff : coeff -> coeff -> bool
+  val eq_formula : formula -> formula -> bool
 end) : sig
-  type key = T.prover_option * (T.coeff Mc.pol * Mc.op1) list
+  type key = T.prover_option * T.formula list
 
   val memo_opt : (unit -> bool) -> string -> (key -> 'a) -> key -> 'a
 end = struct
   module E = struct
-    type t = T.prover_option * (T.coeff Mc.pol * Mc.op1) list
+    type t = T.prover_option * T.formula list
 
     let equal =
       Hash.(
         eq_pair T.eq_prover_option
-          (CList.equal (eq_pair (eq_pol T.eq_coeff) Hash.eq_op1)))
+           (CList.equal T.eq_formula))
 
-    let hash =
-      let hash_cstr = Hash.(hash_pair (hash_pol T.hash_coeff) hash_op1) in
-      Hash.((hash_pair T.hash_prover_option (List.fold_left hash_cstr)) 0)
+    let hash  =
+      Hash.((hash_pair T.hash_prover_option (List.fold_left T.hash_formula)) 0)
   end
 
   include Persistent_cache.PHashtable (E)
@@ -2182,14 +2280,16 @@ end
 
 module CacheCsdp = MakeCache (struct
   type prover_option = provername
-  type coeff = Mc.q
+  type formula = Mc.q Mc.nFormula
 
   let hash_prover_option =
     Hash.(hash_pair hash_string (hash_elt (Option.hash (fun x -> x))))
 
   let eq_prover_option = Hash.(eq_pair String.equal (Option.equal Int.equal))
-  let hash_coeff = Hash.hash_q
-  let eq_coeff = Hash.eq_q
+
+  let hash_formula  = Hash.(hash_pair (hash_pol Hash.hash_q) hash_op1)
+
+  let eq_formula = Hash.(eq_pair (eq_pol eq_q) eq_op1)
 end)
 
 (**
@@ -2248,6 +2348,19 @@ let call_csdpcert_q provername poly =
       print_string "buggy certificate";
       Unknown )
 
+let call_csdpcert_r provername poly =
+  let poly = List.filter_map
+               (fun x -> match x with
+                         | Mc.IsZ _ -> None
+                         | Mc.IsF f -> Some f) poly  in
+  match call_csdpcert provername poly with
+  | None -> Unknown
+  | Some cert ->
+       let cert = Mc.RatProof (Certificate.z_cert_of_pos cert, Mc.DoneProof) in
+       Prf cert
+
+
+
 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
@@ -2332,93 +2445,222 @@ let lift_pexpr_prover p l = p (List.map (fun (e, o) -> (Mc.denorm e, o)) l)
 
 module CacheZ = MakeCache (struct
   type prover_option = bool * bool * int
-  type coeff = Mc.z
+  type formula = Mc.z Mc.nFormula
 
   let hash_prover_option : int -> prover_option -> int =
     Hash.hash_elt Hashtbl.hash
 
   let eq_prover_option : prover_option -> prover_option -> bool = ( = )
-  let eq_coeff = Hash.eq_z
-  let hash_coeff = Hash.hash_z
+
+  let eq_formula = Hash.(eq_pair (eq_pol eq_z) eq_op1)
+  let hash_formula = Hash.(hash_pair (hash_pol hash_z) hash_op1)
 end)
 
+
+module CacheR = MakeCache (struct
+  type prover_option = int
+
+  type formula = (Mc.q Mc.nFormula) Mc.eFormula
+
+  let hash_prover_option : int -> prover_option -> int =
+    Hash.hash_elt Hashtbl.hash
+
+  let eq_prover_option : prover_option -> prover_option -> bool = ( = )
+
+  let eq_formula = eformula_eq Hash.eq_q
+
+  let hash_int = Hash.hash_elt (fun x -> x)
+
+  let hash_formula i e =
+    match e with
+    | Mc.IsZ(b,x) -> Hash.(hash_pair hash_int (hash_elt CoqToCaml.index)  i (0,x))
+    | Mc.IsF f -> Hash.(hash_pair hash_int (hash_pair (hash_pol hash_q) hash_op1) i (1,f))
+end)
+
+
 module CacheQ = MakeCache (struct
   type prover_option = int
-  type coeff = Mc.q
+  type formula = Mc.q Mc.nFormula
 
   let hash_prover_option : int -> int -> int = Hash.hash_elt Hashtbl.hash
   let eq_prover_option = Int.equal
-  let eq_coeff = Hash.eq_q
-  let hash_coeff = Hash.hash_q
+
+  let eq_formula = Hash.(eq_pair (eq_pol eq_q) eq_op1)
+  let hash_formula = Hash.(hash_pair (hash_pol hash_q) hash_op1)
 end)
 
 let memo_lia =
   CacheZ.memo_opt use_lia_cache ".lia.cache" (fun ((_, _, b), s) ->
-      lift_pexpr_prover (Certificate.lia b) s)
+      lift_pexpr_prover (Certificate.lia b ~isZ:None) s)
 
 let memo_nlia =
-  CacheZ.memo_opt use_nia_cache ".nia.cache" (fun ((_, _, b), s) ->
-      lift_pexpr_prover (Certificate.nlia b) s)
+  CacheZ.memo_opt use_nia_cache ".nia.cache" (fun ((_, _, b) , s) ->
+      lift_pexpr_prover (Certificate.nlia b ~isZ:None) s)
+
+
+let rprover (p:?isZ:ISet.t option -> int -> (Mc.z Mc.pExpr * Mc.op1) list -> zres) ((o:int),l) : Certificate.zres =
+  let pexpr_form f = let (f,o) = Mc.nformulaZ f in
+                     (Mc.denorm f, o) in
+
+  let rec xcollect_isZ s acc = function
+    | [] -> s, acc
+    | e::l0 ->
+       (match e with
+        | Mc.IsZ (b, x) ->
+           xcollect_isZ (if b then ISet.add (Mutils.CoqToCaml.positive x) s else s) acc l0
+        | Mc.IsF f -> xcollect_isZ s ((pexpr_form f)::acc) l0) in
+  let (s, l') = xcollect_isZ ISet.empty [] l in
+  p ~isZ:(Some s) o  l'
+
+
+let memo_lra =
+  CacheR.memo_opt use_lra_cache ".lra.cache" (fun (o, s) ->
+      rprover Certificate.lia (o,s))
 
 let memo_nra =
-  CacheQ.memo_opt use_nra_cache ".nra.cache" (fun (o, s) ->
-      lift_pexpr_prover (Certificate.nlinear_prover o) s)
+  CacheR.memo_opt use_nra_cache ".nra.cache" (fun (o, s) ->
+      rprover Certificate.nlia (o,s))
+
+let memo_lqa =
+  CacheQ.memo_opt  use_lqa_cache ".lqa.cache"
+      (fun (o, l) ->
+        lift_pexpr_prover (Certificate.linear_prover_with_cert o) l)
+
+(* For R, the computation is not completly
+   straightforward because the prover (see RMicromega.QCheck)
+   is massaging the clause.
+ *)
+
+(* [hyps_of_rproof cl prf] computes the elements of [cl]
+   that are needed for checking the proof [prf].
+   It simulates the pre-processing which
+   collect the isZ predicates and reverses the order of the isF predicates *)
+
+let hyps_of_rproof cl prf =
+  let rec xcollect_isZ i isZ cli cl =
+    match cl with
+    | [] -> isZ, cli
+    | (e,_)::cl -> match e with
+               | Mc.IsZ(b, _) ->
+                  let isZ' = if b then ISet.add i isZ else isZ in
+                  xcollect_isZ (i+1) isZ' cli cl
+               | Mc.IsF f -> xcollect_isZ (i+1) isZ (i::cli) cl in
+  let (s,cl') = xcollect_isZ 0 ISet.empty [] cl in
+  let iprf  = hyps_of_pt prf in
+  (* iprf gives indices related to cl'. We need to remap towards cl *)
+  let res = ISet.union s (ISet.map (List.nth cl') iprf) in
+  res
+
+
+
+
+
+let rebuild_proof_index eq pre_process cl new_cl =
+  let cl = pre_process cl in
+  let new_cl = List.mapi (fun i (f, _) -> (f, i))  (pre_process new_cl) in
+  let remap_index i =
+    (* Get the formula corresponding to the proof index i *)
+    let f = fst (List.nth cl i) in
+    (* Find the index for the formula f in the new clause cl' *)
+    CList.assoc_f eq f new_cl   in
+
+  let cache = ref IMap.empty in
+  fun i ->
+  try IMap.find i !cache with
+  | Not_found ->
+     let j = remap_index i in
+     cache := IMap.add i j !cache;
+     j
+
+
+let rebuild_proof_index_proof_z  =
+  rebuild_proof_index (nformula_eq Mc.Z.eqb) (fun x -> x)
+
+let rebuild_proof_index_proof_q = rebuild_proof_index (nformula_eq Mc.qeq_bool) (fun x -> x)
+
+let rebuild_proof_index_proof_r =
+  let rec xcollect cli cl =
+    match cl with
+    | [] ->  cli
+    | ((e,_) as f) ::cl -> match e with
+                   | Mc.IsZ(b, _) -> xcollect  cli cl
+                   | Mc.IsF _ -> xcollect  (f::cli) cl in
+  rebuild_proof_index (eformula_eq Mc.qeq_bool) (xcollect [])
+
+
+
 
 let linear_prover_Q =
   { name = "linear prover"
   ; get_option = lra_proof_depth
-  ; prover =
-      (fun (o, l) ->
-        lift_pexpr_prover (Certificate.linear_prover_with_cert o) l)
-  ; hyps = hyps_of_cone
+  ; prover = memo_lqa
+  ; hyps = (fun _ -> hyps_of_cone)
   ; compact = compact_cone
+  ; rebuild_proof_index = rebuild_proof_index (nformula_eq Mc.qeq_bool) (fun x -> x)
   ; 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 = lra_proof_depth
-  ; prover =
-      (fun (o, l) ->
-        lift_pexpr_prover (Certificate.linear_prover_with_cert 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)) }
+  ; prover = memo_lra
+  ; hyps = hyps_of_rproof
+  ; compact = compact_pt
+  ; rebuild_proof_index = rebuild_proof_index_proof_r
+  ; pp_prf = pp_proof_term
+  ; pp_f = (fun o x -> pp_eformula (fun o x -> pp_pol pp_q o (fst x)) o x) }
 
 let nlinear_prover_R =
   { name = "nra"
   ; get_option = lra_proof_depth
   ; prover = memo_nra
-  ; hyps = hyps_of_cone
+  ; hyps = hyps_of_rproof
+  ; compact = compact_pt
+  ; rebuild_proof_index = rebuild_proof_index_proof_r
+  ; pp_prf = pp_proof_term
+  ; pp_f = (fun o x -> pp_eformula (fun o x -> pp_pol pp_q o (fst x)) o x) }
+
+let nlinear_prover_Q =
+  { name = "nqa"
+  ; get_option = lra_proof_depth
+  (* TODO - use cache*)
+  ; prover = (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s)
+  ; hyps = (fun _ -> hyps_of_cone)
+  ; rebuild_proof_index = rebuild_proof_index_proof_q
   ; 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
+  ; hyps = (fun _ -> hyps_of_cone)
   ; compact = compact_cone
+  ; rebuild_proof_index = rebuild_proof_index_proof_q
   ; 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)) }
+  ; prover = (fun (o,l) ->  call_csdpcert_r o l)
+  ; hyps = (fun _ -> hyps_of_pt)
+  ; compact = compact_pt
+  ; rebuild_proof_index = rebuild_proof_index_proof_r
+  ; pp_prf = pp_proof_term
+  ; pp_f = (fun o x -> pp_eformula (fun o x -> pp_pol pp_q o (fst x)) o 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
+  ; hyps = (fun _ -> hyps_of_pt)
   ; compact = compact_pt
+  ; rebuild_proof_index = rebuild_proof_index_proof_z
   ; pp_prf = pp_proof_term
   ; pp_f = (fun o x -> pp_pol pp_z o (fst x)) }
 
@@ -2426,8 +2668,9 @@ let linear_Z =
   { name = "lia"
   ; get_option = get_lia_option
   ; prover = memo_lia
-  ; hyps = hyps_of_pt
+  ; hyps = (fun _ -> hyps_of_pt)
   ; compact = compact_pt
+  ; rebuild_proof_index = rebuild_proof_index_proof_z
   ; pp_prf = pp_proof_term
   ; pp_f = (fun o x -> pp_pol pp_z o (fst x)) }
 
@@ -2435,8 +2678,9 @@ let nlinear_Z =
   { name = "nlia"
   ; get_option = get_lia_option
   ; prover = memo_nlia
-  ; hyps = hyps_of_pt
+  ; hyps = (fun _ -> hyps_of_pt)
   ; compact = compact_pt
+  ; rebuild_proof_index = rebuild_proof_index_proof_z
   ; pp_prf = pp_proof_term
   ; pp_f = (fun o x -> pp_pol pp_z o (fst x)) }
 
@@ -2452,107 +2696,91 @@ let exfalso_if_concl_not_Prop =
           Tacticals.tclIDTAC
         else Tactics.exfalso))
 
-let micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac =
+let micromega_gen parse_arith  cnf spec prover tac =
   Tacticals.tclTHEN exfalso_if_concl_not_Prop
-    (micromega_gen parse_arith pre_process cnf spec dumpexpr prover tac)
+    (micromega_gen parse_arith cnf spec prover tac)
 
-let micromega_genr prover tac =
-  Tacticals.tclTHEN exfalso_if_concl_not_Prop (micromega_genr prover tac)
+let micromega_genr spec prover tac =
+  Tacticals.tclTHEN exfalso_if_concl_not_Prop (micromega_genr spec prover tac)
 
 let xlra_Q =
   micromega_gen parse_qarith
-    (fun _ x -> x)
-    Mc.cnfQ qq_domain_spec dump_qexpr linear_prover_Q
+    Mc.cnfQ qq_domain_spec  linear_prover_Q
 
 let wlra_Q =
   micromega_wit_gen
-    (fun _ x -> x)
     Mc.cnfQ qq_domain_spec linear_prover_Q
 
-let xlra_R = micromega_genr linear_prover_R
+let xlra_R = micromega_genr rzdomain linear_prover_R
 
 let xlia =
   micromega_gen parse_zarith
-    (fun _ x -> x)
-    Mc.cnfZ zz_domain_spec dump_zexpr linear_Z
+    Mc.cnfZ zz_domain_spec  linear_Z
 
 let wlia =
   micromega_wit_gen
-    (fun _ x -> x)
     Mc.cnfZ zz_domain_spec linear_Z
 
 let xnra_Q =
   micromega_gen parse_qarith
-    (fun _ x -> x)
-    Mc.cnfQ qq_domain_spec dump_qexpr nlinear_prover_R
+    Mc.cnfQ qq_domain_spec  nlinear_prover_Q
 
 let wnra_Q =
   micromega_wit_gen
-    (fun _ x -> x)
-    Mc.cnfQ qq_domain_spec nlinear_prover_R
+    Mc.cnfQ qq_domain_spec nlinear_prover_Q
 
-let xnra_R = micromega_genr nlinear_prover_R
+let xnra_R = micromega_genr rzdomain nlinear_prover_R
 
 let xnia =
   micromega_gen parse_zarith
-    (fun _ x -> x)
-    Mc.cnfZ zz_domain_spec dump_zexpr nlinear_Z
+    Mc.cnfZ zz_domain_spec  nlinear_Z
 
 let wnia =
   micromega_wit_gen
-    (fun _ x -> x)
     Mc.cnfZ zz_domain_spec nlinear_Z
 
 let xsos_Q =
   micromega_gen parse_qarith
-    (fun _ x -> x)
-    Mc.cnfQ qq_domain_spec dump_qexpr
+    Mc.cnfQ qq_domain_spec
     (non_linear_prover_Q "pure_sos" None)
 
 let wsos_Q =
   micromega_wit_gen
-    (fun _ x -> x)
     Mc.cnfQ qq_domain_spec
     (non_linear_prover_Q "pure_sos" None)
 
-let xsos_R = micromega_genr (non_linear_prover_R "pure_sos" None)
+let xsos_R = micromega_genr rzdomain (non_linear_prover_R "pure_sos" None)
 
 let xsos_Z =
   micromega_gen parse_zarith
-    (fun _ x -> x)
-    Mc.cnfZ zz_domain_spec dump_zexpr
+    Mc.cnfZ zz_domain_spec
     (non_linear_prover_Z "pure_sos" None)
 
 let wsos_Z =
   micromega_wit_gen
-    (fun _ x -> x)
     Mc.cnfZ zz_domain_spec
     (non_linear_prover_Z "pure_sos" None)
 
 let xpsatz_Q i =
   micromega_gen parse_qarith
-    (fun _ x -> x)
-    Mc.cnfQ qq_domain_spec dump_qexpr
+    Mc.cnfQ qq_domain_spec
     (non_linear_prover_Q "real_nonlinear_prover" (Some i))
 
 let wpsatz_Q i =
   micromega_wit_gen
-    (fun _ x -> x)
     Mc.cnfQ qq_domain_spec
     (non_linear_prover_Q "real_nonlinear_prover" (Some i))
 
 let xpsatz_R i =
-  micromega_genr (non_linear_prover_R "real_nonlinear_prover" (Some i))
+  micromega_genr rzdomain (non_linear_prover_R "real_nonlinear_prover" (Some i))
 
 let xpsatz_Z i =
   micromega_gen parse_zarith
-    (fun _ x -> x)
-    Mc.cnfZ zz_domain_spec dump_zexpr
+    Mc.cnfZ zz_domain_spec
     (non_linear_prover_Z "real_nonlinear_prover" (Some i))
 
 let wpsatz_Z i =
   micromega_wit_gen
-    (fun _ x -> x)
     Mc.cnfZ zz_domain_spec
     (non_linear_prover_Z "real_nonlinear_prover" (Some i))
 
diff --git a/plugins/micromega/g_zify.mlg b/plugins/micromega/g_zify.mlg
index e7da486cb744..bfc83778d1e6 100644
--- a/plugins/micromega/g_zify.mlg
+++ b/plugins/micromega/g_zify.mlg
@@ -16,41 +16,129 @@ open Tacarg
 
 let locality = Zify.zify_register_locality
 
+let deprecate_zify_tac zify_tac tify_tac =
+    CWarnings.create ~name:zify_tac ~category:Deprecation.Version.v9_1
+    (fun () -> Pp.(str "The tactic " ++ str zify_tac ++ str " is deprecated. Use " ++ str tify_tac ++ str " instead."))
+
+let deprecate_zify_vernac cmd1 cmd2  =
+        CWarnings.create ~name:(cmd1^" Zify "^cmd2) ~category:Deprecation.Version.v9_1
+        (fun () -> Pp.(
+         str cmd1 ++ str " Zify "++ str cmd2 ++ str " is deprecated. Use "++ str cmd1 ++ str " Tify "++ str cmd2 ++ str " instead."))
+
+let deprecate_zify_iter_specs = deprecate_zify_tac "zify_iter_specs" "tify_iter_specs"
+let deprecate_zify_iter_let = deprecate_zify_tac "zify_iter_let" "tify_iter_let"
+let deprecate_zify_elim_let = deprecate_zify_tac "zify_elim_let" "tify_elim_let"
+let deprecate_zify_op = deprecate_zify_tac "zify_op" "tify_op Z"
+let deprecate_zify_saturate = deprecate_zify_tac "zify_saturate" "tify_saturate"
+
+let deprecate_Add_InjTyp = deprecate_zify_vernac "Add" "InjTyp"
+let deprecate_Add_BinOp  = deprecate_zify_vernac "Add" "BinOp"
+let deprecate_Add_UnOp   = deprecate_zify_vernac "Add" "UnOp"
+let deprecate_Add_CstOp  = deprecate_zify_vernac "Add" "CstOp"
+let deprecate_Add_BinRel = deprecate_zify_vernac "Add" "BinRel"
+let deprecate_Add_PropOp = deprecate_zify_vernac "Add" "PropOp"
+let deprecate_Add_PropBinOp = deprecate_zify_vernac "Add" "PropBinOp"
+let deprecate_Add_PropUOp   = deprecate_zify_vernac "Add" "PropUOp"
+let deprecate_Add_BinOpSpec = deprecate_zify_vernac "Add" "BinOpSpec"
+let deprecate_Add_UnOpSpec  = deprecate_zify_vernac "Add" "UnOpSpec"
+let deprecate_Add_Saturate  = deprecate_zify_vernac "Add" "Saturate"
+
+let deprecate_Show_InjTyp = deprecate_zify_vernac "Show" "InjTyp"
+let deprecate_Show_BinOp  = deprecate_zify_vernac "Show" "BinOp"
+let deprecate_Show_UnOp   = deprecate_zify_vernac "Show" "UnOp"
+let deprecate_Show_CstOp  = deprecate_zify_vernac "Show" "CstOp"
+let deprecate_Show_BinRel = deprecate_zify_vernac "Show" "BinRel"
+let deprecate_Show_BinOpSpec = deprecate_zify_vernac "Show" "BinOpSpec"
+let deprecate_Show_UnOpSpec  = deprecate_zify_vernac "Show" "UnOpSpec"
+
 }
 
 DECLARE PLUGIN "rocq-runtime.plugins.zify"
 
 VERNAC COMMAND EXTEND DECLAREINJECTION CLASSIFIED AS SIDEFF
-| #[ locality ] ["Add" "Zify" "InjTyp"   reference(t) ] -> { Zify.InjTable.register locality t }
-| #[ locality ] ["Add" "Zify" "BinOp"     reference(t) ] -> { Zify.BinOp.register locality t }
-| #[ locality ] ["Add" "Zify" "UnOp"      reference(t) ] -> { Zify.UnOp.register locality t }
-| #[ locality ] ["Add" "Zify" "CstOp"     reference(t) ] -> { Zify.CstOp.register locality t }
-| #[ locality ] ["Add" "Zify" "BinRel"    reference(t) ] -> { Zify.BinRel.register locality t }
-| #[ locality ] ["Add" "Zify" "PropOp"    reference(t) ] -> { Zify.PropBinOp.register locality t }
-| #[ locality ] ["Add" "Zify" "PropBinOp"    reference(t) ] -> { Zify.PropBinOp.register locality t }
-| #[ locality ] ["Add" "Zify" "PropUOp"   reference(t) ] -> { Zify.PropUnOp.register locality t }
-| #[ locality ] ["Add" "Zify" "BinOpSpec" reference(t) ] -> { Zify.BinOpSpec.register locality t }
-| #[ locality ] ["Add" "Zify" "UnOpSpec"  reference(t) ] -> { Zify.UnOpSpec.register locality t }
-| #[ locality ] ["Add" "Zify" "Saturate"  reference(t) ] -> { Zify.Saturate.register locality t }
+| #[ locality ] ["Add" "Zify" "InjTyp"   reference(t) ] -> {
+  deprecate_Add_InjTyp (); Zify.InjTable.register locality t }
+| #[ locality ] ["Add" "Zify" "BinOp"     reference(t) ] -> {
+  deprecate_Add_BinOp (); Zify.BinOp.register locality t }
+| #[ locality ] ["Add" "Zify" "UnOp"      reference(t) ] -> {
+  deprecate_Add_UnOp (); Zify.UnOp.register locality t }
+| #[ locality ] ["Add" "Zify" "CstOp"     reference(t) ] -> {
+  deprecate_Add_CstOp (); Zify.CstOp.register locality t }
+| #[ locality ] ["Add" "Zify" "BinRel"    reference(t) ] -> {
+  deprecate_Add_BinRel (); Zify.BinRel.register locality t }
+| #[ locality ] ["Add" "Zify" "PropOp"    reference(t) ] -> {
+  deprecate_Add_PropOp (); Zify.PropBinOp.register locality t }
+| #[ locality ] ["Add" "Zify" "PropBinOp"    reference(t) ] -> {
+  deprecate_Add_PropBinOp (); Zify.PropBinOp.register locality t }
+| #[ locality ] ["Add" "Zify" "PropUOp"   reference(t) ] -> {
+    deprecate_Add_PropUOp (); Zify.PropUnOp.register locality t }
+| #[ locality ] ["Add" "Zify" "BinOpSpec" reference(t) ] -> {
+  deprecate_Add_BinOpSpec (); Zify.BinOpSpec.register locality t }
+| #[ locality ] ["Add" "Zify" "UnOpSpec"  reference(t) ] -> {
+  deprecate_Add_UnOpSpec (); Zify.UnOpSpec.register locality t }
+| #[ locality ] ["Add" "Zify" "Saturate"  reference(t) ] -> {
+  deprecate_Add_Saturate (); Zify.Saturate.register locality t }
 END
 
+VERNAC COMMAND EXTEND TIFYDECLAREINJECTION CLASSIFIED AS SIDEFF
+| #[ locality ] ["Add" "Tify" "InjTyp"   reference(t) ] -> { Zify.InjTable.register locality t }
+| #[ locality ] ["Add" "Tify" "BinOp"     reference(t) ] -> { Zify.BinOp.register locality t }
+| #[ locality ] ["Add" "Tify" "UnOp"      reference(t) ] -> { Zify.UnOp.register locality t }
+| #[ locality ] ["Add" "Tify" "CstOp"     reference(t) ] -> { Zify.CstOp.register locality t }
+| #[ locality ] ["Add" "Tify" "BinRel"    reference(t) ] -> { Zify.BinRel.register locality t }
+| #[ locality ] ["Add" "Tify" "PropOp"    reference(t) ] -> { Zify.PropBinOp.register locality t }
+| #[ locality ] ["Add" "Tify" "PropBinOp"    reference(t) ] -> { Zify.PropBinOp.register locality t }
+| #[ locality ] ["Add" "Tify" "PropUOp"   reference(t) ] -> { Zify.PropUnOp.register locality t }
+| #[ locality ] ["Add" "Tify" "BinOpSpec" reference(t) ] -> { Zify.BinOpSpec.register locality t }
+| #[ locality ] ["Add" "Tify" "UnOpSpec"  reference(t) ] -> { Zify.UnOpSpec.register locality t }
+| #[ locality ] ["Add" "Tify" "Saturate"  reference(t) ] -> { Zify.Saturate.register locality t }
+END
+
+
 TACTIC EXTEND ITER
-| [ "zify_iter_specs"] -> { Zify.iter_specs}
+| [ "zify_iter_specs"] -> {
+  deprecate_zify_iter_specs (); Zify.iter_specs}
+| [ "tify_iter_specs"] -> { Zify.iter_specs}
 END
 
 TACTIC EXTEND TRANS
-| [ "zify_op"  ] -> { Zify.zify_tac }
-| [ "zify_saturate"  ] -> { Zify.saturate }
-| [ "zify_iter_let" tactic(t)] -> { Zify.iter_let t }
-| [ "zify_elim_let" ] -> { Zify.elim_let }
+| [ "zify_op"  ] -> {
+    deprecate_zify_op () ; Zify.zify_op ()}
+| [ "zify_saturate"  ] -> {
+    deprecate_zify_saturate () ; Zify.saturate }
+| [ "zify_iter_let" tactic(t)] -> {
+    deprecate_zify_iter_let (); Zify.iter_let t }
+| [ "zify_elim_let" ] -> {
+  deprecate_zify_elim_let (); Zify.elim_let }
+| [ "tify_op" reference(t) ] -> { Zify.tify_op t}
+| [ "tify_saturate"  ] -> { Zify.saturate }
+| [ "tify_iter_let" tactic(t)] -> { Zify.iter_let t }
+| [ "tify_elim_let" ] -> { Zify.elim_let }
 END
 
 VERNAC COMMAND EXTEND ZifyPrint CLASSIFIED AS SIDEFF
-|[ "Show" "Zify" "InjTyp" ] -> { Zify.InjTable.print () }
-|[ "Show" "Zify" "BinOp" ]  -> { Zify.BinOp.print () }
-|[ "Show" "Zify" "UnOp" ]   -> { Zify.UnOp.print () }
-|[ "Show" "Zify" "CstOp"]   -> { Zify.CstOp.print () }
-|[ "Show" "Zify" "BinRel"]  -> { Zify.BinRel.print () }
-|[ "Show" "Zify" "UnOpSpec"] -> { Zify.UnOpSpec.print() }
-|[ "Show" "Zify" "BinOpSpec"] -> { Zify.BinOpSpec.print() }
+|[ "Show" "Zify" "InjTyp" ] -> {
+   deprecate_Show_InjTyp (); Zify.InjTable.print () }
+|[ "Show" "Zify" "BinOp" ]  -> {
+   deprecate_Show_BinOp (); Zify.BinOp.print () }
+|[ "Show" "Zify" "UnOp" ]   -> {
+   deprecate_Show_UnOp (); Zify.UnOp.print () }
+|[ "Show" "Zify" "CstOp"]   -> {
+   deprecate_Show_CstOp (); Zify.CstOp.print () }
+|[ "Show" "Zify" "BinRel"]  -> {
+    deprecate_Show_BinRel (); Zify.BinRel.print () }
+|[ "Show" "Zify" "UnOpSpec"] -> {
+   deprecate_Show_UnOpSpec (); Zify.UnOpSpec.print() }
+|[ "Show" "Zify" "BinOpSpec"] -> {
+   deprecate_Show_BinOpSpec (); Zify.BinOpSpec.print() }
+END
+
+VERNAC COMMAND EXTEND TifyPrint CLASSIFIED AS SIDEFF
+|[ "Show" "Tify" "InjTyp" ] -> { Zify.InjTable.print () }
+|[ "Show" "Tify" "BinOp" ]  -> { Zify.BinOp.print () }
+|[ "Show" "Tify" "UnOp" ]   -> { Zify.UnOp.print () }
+|[ "Show" "Tify" "CstOp"]   -> { Zify.CstOp.print () }
+|[ "Show" "Tify" "BinRel"]  -> { Zify.BinRel.print () }
+|[ "Show" "Tify" "UnOpSpec"] -> { Zify.UnOpSpec.print() }
+|[ "Show" "Tify" "BinOpSpec"] -> { Zify.BinOpSpec.print() }
 END
diff --git a/plugins/micromega/inf.ml b/plugins/micromega/inf.ml
new file mode 100644
index 000000000000..d4df88af9c06
--- /dev/null
+++ b/plugins/micromega/inf.ml
@@ -0,0 +1,105 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \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)         *)
+(************************************************************************)
+
+open NumCompat
+open Q.Notations
+open Mutils
+
+(** Manipulation of infinitesimals *)
+
+(* (x,y) denotes x + y.e for some infinitesimal e *)
+type t = Q.t * Q.t
+
+let tolerance = ref (Q.of_float min_float)
+
+let set_tolerance q = tolerance := q
+
+let frac_num (x,y) =
+  let fn = x -/ Q.floor x in
+  if not (y =/ Q.zero)
+  then Some (fn +/ !tolerance)
+  else if fn =/ Q.zero
+       then None
+       else Some fn
+
+let decomp (x,y) = (x,y)
+
+let cst q = (q,Q.zero)
+
+let zero = (Q.zero,Q.zero)
+
+let epsilon = (Q.zero, Q.one)
+
+let cste q b =
+  if b
+  then  (q,Q.minus_one)
+  else  (q,Q.zero)
+
+let hash (x,y) = Hashtbl.hash (Q.to_float x,Q.to_float y)
+
+let add (a1,b1) (a2,b2) =
+  (a1 +/ a2, b1 +/ b2)
+
+let mulc c (a1,b1) = (c */ a1, c */ b1)
+
+let divc (a1,b1) c = (a1 // c , b1 // c)
+
+let uminus (a1,b1) = (Q.neg a1,Q.neg b1)
+
+let abs (i,j) =
+  let cmp = Q.compare i Q.zero in
+  if cmp = 0
+  then (Q.zero,Q.abs j) (* epsilon wins *)
+  else (* sign of epsilon does not matter *)
+    if cmp < 0
+    then (Q.neg i, Q.neg j)
+    else (i,j)
+
+
+let lt (a1,b1) (a2,b2) =
+  let cmp = Q.compare a1 a2 in
+  cmp < 0 || (Int.equal cmp  0 && b1 </ b2)
+
+let ge_0 (a1,b1) =
+  let cmp = Q.compare a1 Q.zero in
+  if cmp > 0 then true
+  else if cmp < 0 then false
+  else b1 >=/ Q.zero
+
+
+let equal (a1,b1) (a2,b2) =
+  a1 =/ a2 && b1 =/ b2
+
+let compare (a1,b1) (a2,b2) =
+  let cmp = Q.compare a1 a2 in
+  if cmp = 0 then Q.compare b1 b2
+  else cmp
+
+let pp o (a1,b1) =
+  match a1 =/ Q.zero , b1 =/ Q.zero with
+  | true , true -> output_string o "0"
+  | true , false -> Printf.fprintf o "%s.e" (Q.to_string b1)
+  | false , true -> output_string o (Q.to_string a1)
+  | false , false -> Printf.fprintf o "%s + %s.e" (Q.to_string a1) (Q.to_string b1)
+
+let is_zero (a1,b1) = a1 =/ Q.zero && (b1 = Q.zero)
+
+let pp_smt o (a1,b1) =
+  match a1 =/ Q.zero , b1 =/ Q.zero with
+  | true , true -> output_string o "0"
+  | true , false -> Printf.fprintf o "(* %a e)" pp_smt_num b1
+  | false , true -> output_string o (Q.to_string a1)
+  | false , false -> Printf.fprintf o "(+ %a  (* %a e))" pp_smt_num a1 pp_smt_num b1
+
+
+let gcd (a,b) =
+  Z.gcd (Q.num a) (Q.num b)
+
+let ppcm (a,b) = Z.ppcm (Q.den a) (Q.den b)
diff --git a/plugins/micromega/inf.mli b/plugins/micromega/inf.mli
new file mode 100644
index 000000000000..f99cf561f885
--- /dev/null
+++ b/plugins/micromega/inf.mli
@@ -0,0 +1,83 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \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)         *)
+(************************************************************************)
+
+open NumCompat
+
+(** a + b.e where a and b are rationals and e > 0  *)
+type t
+
+(** [set_tolerance ()] set a rational used to concretise e.
+    (This is used to get a fractional part in Q.t)
+ *)
+val set_tolerance : Q.t -> unit
+
+(** [decomp (a + b.e)] returns  [(a,b)] *)
+val decomp :  t -> Q.t * Q.t
+
+(** [cst q] returns q + 0.e *)
+val cst : Q.t -> t
+
+(** [zero] is (0 + 0.e) *)
+val zero : t
+
+(** [epsilon] is (0 + 1.e) *)
+val epsilon : t
+
+(** [cste c strict] = if strict then c - 1.e else c + 0.e *)
+val cste : Q.t -> bool -> t
+
+(** [hash x] returns a hash *)
+val hash : t -> int
+
+(** [add (a1+b1.e) (a2+b2.e)] returns a1+a2 + (b1_b2).e *)
+val add : t -> t -> t
+
+(** [mulc c (a+b.e)] returns c*a + c*b.e *)
+val mulc : Q.t -> t -> t
+
+(** [divc (a+b.e) c] returns a/c + b/c.e *)
+val divc : t -> Q.t -> t
+
+(** [uminus (a+b.e)] returns -a + -b.e *)
+val uminus : t -> t
+
+(** [lt (a1+b1.e) (a2+b2.e)] returns a1 < a2 \/ a1 = a2 /\ b1 < b2 *)
+val lt : t -> t -> bool
+
+(** [abs (a+b.e)] returns (a+b.e) < 0 then (-a-b.e) else (a+b.e) *)
+val abs : t -> t
+
+(** [ge_0 (a1+b1.e)] compares with (0+0.e) *)
+val  ge_0 : t -> bool
+
+(** [equal (a1+b1.e) (a2+b2.e)] holds iff a1 = a2 /\ b1 = b2 *)
+val equal : t -> t -> bool
+
+(** [compare] provides a total ordering *)
+val compare : t -> t -> int
+
+(** [pp o (a1+b1.e)] outputs on out_channel [o] a textual representation *)
+val pp : out_channel -> t -> unit
+
+(** [pp_smt  o (a1+b1.e)] outputs on out_channel [o] a smt-lib textual representation *)
+val pp_smt : out_channel -> t -> unit
+
+
+(** [is_zero (a+b.e)] holds if a = b = 0 *)
+val is_zero : t -> bool
+
+(** [gcd (a/a'+b/b'.e)] returns the gcd(a,b) *)
+val gcd : t -> Z.t
+
+(** [ppcm (a/a'+b/b'.e)] returns ppcm(a',b') *)
+val ppcm : t -> Z.t
+
+(** [frac_num a+b.e] returns the fractional part of a+b.e *)
+val frac_num : t -> Q.t option
diff --git a/plugins/micromega/infVect.ml b/plugins/micromega/infVect.ml
new file mode 100644
index 000000000000..c148b16e1e24
--- /dev/null
+++ b/plugins/micromega/infVect.ml
@@ -0,0 +1,101 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \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)         *)
+(************************************************************************)
+
+(** Extend the vector type with an infinitesimal constant,
+    This is need to turn a strict inequality e > 0
+    into a weak inequality e - ϵ >= 0 for some ϵ > 0
+ *)
+open NumCompat
+open Q.Notations
+
+
+type var = int
+type t = Inf.t * Vect.t
+type vector = t
+
+let hash (i1,v1)  =
+  Hashtbl.hash (Inf.hash i1,Vect.hash v1)
+
+let equal (i1,v1) (i2,v2) =
+  Inf.equal i1 i2 && Vect.equal v1 v2
+
+let compare (i1,v1) (i2,v2) =
+  let cmp = Inf.compare i1 i2 in
+  if cmp = 0 then Vect.compare v1 v2
+  else cmp
+
+let pp_gen pp_var o (i,v) =
+  match Inf.is_zero i , Vect.is_null v with
+  | true , true   -> output_string o "0"
+  | true , false  -> Vect.pp_gen pp_var o v
+  | false , true  -> Inf.pp o i
+  | false , false -> Printf.fprintf o "%a+%a" Inf.pp i (Vect.pp_gen pp_var) v
+
+let pp_var o v = Printf.fprintf o "x%i" v
+
+let pp o v = pp_gen pp_var o v
+
+let pp_smt o (i,v) =
+  Printf.fprintf o "(+ %a %a)" Inf.pp_smt i Vect.pp_smt v
+
+let variables (i,v) = Vect.variables v
+
+let get_cst (i,v) = i
+
+let decomp_cst (i,v) = (i,v)
+
+let cst q = (Inf.cst q,Vect.null)
+
+let is_constant (_,v) = Vect.is_null v
+
+
+let null = (Inf.zero,Vect.null)
+
+let is_null (i,v) = Inf.equal Inf.zero i  && Vect.is_null v
+
+let get vr (_,v) = Vect.get vr v
+
+let set vr q (i,v) = (i,Vect.set vr q v)
+
+let update vr f (i,v) = (i,Vect.update vr f v)
+
+let fresh (i,v) = Vect.fresh v
+
+
+let gcd (i,l) =
+  Z.gcd (Inf.gcd i) (Vect.gcd l)
+
+let normalise (i,l) =
+  let (gcd,ppcm) = Vect.fold (fun (g,p) _ n -> (Z.gcd g (Q.num n) , Z.ppcm p (Q.den n))) (Z.zero,Z.one) l in
+  let m = Q.of_bigint ppcm // Q.of_bigint gcd in
+  if m =/ Q.one
+  then  (i,l)
+  else (Inf.mulc m i, Vect.mul m l)
+
+let add (c1,v1) (c2,v2) =
+  (Inf.add c1 c2, Vect.add v1 v2)
+
+let mul q (i,v) = (Inf.mulc q i, Vect.mul q v)
+
+let mul_add c1 (i1,v1) c2 (i2,v2) =
+  (Inf.add (Inf.mulc c1 i1) (Inf.mulc c2 i2),
+   Vect.mul_add c1 v1 c2 v2)
+
+let subst x (i,v) (i',v') =
+  let (n,r) = Vect.subst x v v' in
+  (Inf.add i' (Inf.mulc n i),r)
+
+let uminus (i,v) = (Inf.uminus i, Vect.uminus v)
+
+let of_vect v strict =
+  let (c,v) = Vect.decomp_cst v in
+  (Inf.cste c strict,v)
+
+let of_cst c = (c,Vect.null)
diff --git a/plugins/micromega/infVect.mli b/plugins/micromega/infVect.mli
new file mode 100644
index 000000000000..d2618e9b23ed
--- /dev/null
+++ b/plugins/micromega/infVect.mli
@@ -0,0 +1,120 @@
+(************************************************************************)
+(*         *      The Rocq Prover / The Rocq Development Team           *)
+(*  v      *         Copyright INRIA, CNRS and contributors             *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(*   \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)         *)
+(************************************************************************)
+
+open NumCompat
+open Mutils
+
+(** Variables are simply (positive) integers. *)
+type var = int
+
+(** The type of vectors or equivalently linear expressions.
+           The current implementation is using association lists.
+           A list [(0,c),(x1,ai),...,(xn,an)] represents the linear expression
+           c + a1.xn + ... an.xn where ai are rational constants and xi are variables.
+
+           Note that the variable 0 has a special meaning and represent a constant.
+           Moreover, the representation is spare and variables with a zero coefficient
+           are not represented.
+        *)
+type t
+
+type vector = t
+
+(** {1 Generic functions}  *)
+
+(** [hash] [equal] and [compare] so that Vect.t can be used as
+    keys for Set Map and Hashtbl *)
+
+val hash : t -> int
+val equal : t -> t -> bool
+val compare : t -> t -> int
+
+(** {1 Basic accessors and utility functions} *)
+
+(** [pp_gen pp_var o v] prints the representation of the vector [v] over the channel [o] *)
+val pp_gen : (out_channel -> var -> unit) -> out_channel -> t -> unit
+
+(** [pp o v] prints the representation of the vector [v] over the channel [o] *)
+val pp : out_channel -> t -> unit
+
+(** [pp_smt o v] prints the representation of the vector [v] over the channel [o] using SMTLIB conventions *)
+val pp_smt : out_channel -> t -> unit
+
+(** [variables v] returns the set of variables with non-zero coefficients *)
+val variables : t -> ISet.t
+
+(** [get_cst v] returns c i.e. the coefficient of the variable zero *)
+val get_cst : t -> Inf.t
+
+(** [decomp_cst v] returns the pair (c,a1.x1+...+an.xn) *)
+val decomp_cst : t -> Inf.t * Vect.t
+
+(** [cst c] returns the vector v=c+0.e + 0.x1+...+0.xn *)
+val cst : Q.t -> t
+
+(** [of_cst c] returns the vector v=c + 0.x1+...+0.xn *)
+val of_cst : Inf.t -> t
+
+
+(** [of_vect a1.x1+...+an.xn b ] returns the vector v = 0 - b.e + a1.x1+...+an.xn*)
+val of_vect : Vect.t -> bool -> t
+
+(** [is_constant v] holds if [v] is a constant vector i.e. v=c+0.x1+...+0.xn
+ *)
+val is_constant : t -> bool
+
+(** [null] is the empty vector i.e. 0+0.x1+...+0.xn *)
+val null : t
+
+(** [is_null v] returns whether [v] is the [null] vector i.e [equal v  null] *)
+val is_null : t -> bool
+
+(** [get xi v] returns the coefficient ai of the variable [xi]. *)
+val get : var -> t -> Q.t
+
+(** [set xi ai' v] returns the vector c+a1.x1+...ai'.xi+...+an.xn
+    i.e. the coefficient of the variable xi is set to ai' *)
+val set : var -> Q.t -> t -> t
+
+(** [update xi f v] returns c+a1.x1+...+f(ai).xi+...+an.xn *)
+val update : var -> (Q.t -> Q.t) -> t -> t
+
+(** [fresh v] return the fresh variable with index 1+ max (variables v) *)
+val fresh : t -> int
+
+(** [gcd v] returns gcd(num(c),num(a1),...,num(an)) where num extracts
+   the numerator of a rational value. *)
+val gcd : t -> Z.t
+
+(** [normalise v] returns a vector with only integer coefficients *)
+val normalise : t -> t
+
+(** {1 Linear arithmetics} *)
+
+(** [add v1 v2] is vector addition.
+    @param v1 is of the form c +a1.x1  +...+an.xn
+    @param v2 is of the form c'+a1'.x1 +...+an'.xn
+    @return c1+c1'+ (a1+a1').x1 + ... + (an+an').xn
+ *)
+val add : t -> t -> t
+
+(** [mul a v] is vector multiplication of vector [v] by a scalar [a].
+    @return a.v = a.c+a.a1.x1+...+a.an.xn *)
+val mul : Q.t -> t -> t
+
+(** [mul_add c1 v1 c2 v2] returns the linear combination c1.v1+c2.v2 *)
+val mul_add : Q.t -> t -> Q.t -> t -> t
+
+(** [subst x v v'] replaces x by v in vector v' and also returns the coefficient of x in v' *)
+val subst : int -> t -> t -> t
+
+(** [uminus v]
+    @return -v the opposite vector of v i.e. (-1).v  *)
+val uminus : t -> t
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index ede8497a9ec3..a4cbb71960f9 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -1,6 +1,3 @@
-(* *** DO NOT EDIT *** *)
-(* This file is extracted from test-suite/output/MExtraction.v in the stdlib *)
-(* *** DO NOT EDIT *** *)
 
 type __ = Obj.t
 
@@ -60,6 +57,12 @@ module Coq__1 = struct
 end
 include Coq__1
 
+(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
+
+let rec map f = function
+| [] -> []
+| a::l0 -> (f a)::(map f l0)
+
 (** val nth : nat -> 'a1 list -> 'a1 -> 'a1 **)
 
 let rec nth n0 l default =
@@ -78,12 +81,6 @@ let rec rev_append l l' =
   | [] -> l'
   | a::l0 -> rev_append l0 (a::l')
 
-(** val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list **)
-
-let rec map f = function
-| [] -> []
-| a::l0 -> (f a)::(map f l0)
-
 (** val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1 **)
 
 let rec fold_left f l a0 =
@@ -113,10 +110,121 @@ type z =
 
 module Pos =
  struct
+  (** val succ : positive -> positive **)
+
+  let rec succ = function
+  | XI p -> XO (succ p)
+  | XO p -> XI p
+  | XH -> XO XH
+
+  (** val add : positive -> positive -> positive **)
+
+  let rec add x y =
+    match x with
+    | XI p ->
+      (match y with
+       | XI q0 -> XO (add_carry p q0)
+       | XO q0 -> XI (add p q0)
+       | XH -> XO (succ p))
+    | XO p ->
+      (match y with
+       | XI q0 -> XI (add p q0)
+       | XO q0 -> XO (add p q0)
+       | XH -> XI p)
+    | XH -> (match y with
+             | XI q0 -> XO (succ q0)
+             | XO q0 -> XI q0
+             | XH -> XO XH)
+
+  (** val add_carry : positive -> positive -> positive **)
+
+  and add_carry x y =
+    match x with
+    | XI p ->
+      (match y with
+       | XI q0 -> XI (add_carry p q0)
+       | XO q0 -> XO (add_carry p q0)
+       | XH -> XI (succ p))
+    | XO p ->
+      (match y with
+       | XI q0 -> XO (add_carry p q0)
+       | XO q0 -> XI (add p q0)
+       | XH -> XO (succ p))
+    | XH ->
+      (match y with
+       | XI q0 -> XI (succ q0)
+       | XO q0 -> XO (succ q0)
+       | XH -> XI XH)
+
+  (** val pred_double : positive -> positive **)
+
+  let rec pred_double = function
+  | XI p -> XI (XO p)
+  | XO p -> XI (pred_double p)
+  | XH -> XH
+
   type mask =
   | IsNul
   | IsPos of positive
   | IsNeg
+
+  (** val mul : positive -> positive -> positive **)
+
+  let rec mul x y =
+    match x with
+    | XI p -> add y (XO (mul p y))
+    | XO p -> XO (mul p y)
+    | XH -> y
+
+  (** val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1 **)
+
+  let rec iter f x = function
+  | XI n' -> f (iter f (iter f x n') n')
+  | XO n' -> iter f (iter f x n') n'
+  | XH -> f x
+
+  (** val compare_cont : comparison -> positive -> positive -> comparison **)
+
+  let rec compare_cont r x y =
+    match x with
+    | XI p ->
+      (match y with
+       | XI q0 -> compare_cont r p q0
+       | XO q0 -> compare_cont Gt p q0
+       | XH -> Gt)
+    | XO p ->
+      (match y with
+       | XI q0 -> compare_cont Lt p q0
+       | XO q0 -> compare_cont r p q0
+       | XH -> Gt)
+    | XH -> (match y with
+             | XH -> r
+             | _ -> Lt)
+
+  (** val compare : positive -> positive -> comparison **)
+
+  let compare =
+    compare_cont Eq
+
+  (** val eqb : positive -> positive -> bool **)
+
+  let rec eqb p q0 =
+    match p with
+    | XI p2 -> (match q0 with
+                | XI q1 -> eqb p2 q1
+                | _ -> false)
+    | XO p2 -> (match q0 with
+                | XO q1 -> eqb p2 q1
+                | _ -> false)
+    | XH -> (match q0 with
+             | XH -> true
+             | _ -> false)
+
+  (** val of_succ_nat : nat -> positive **)
+
+  let rec of_succ_nat = function
+  | O -> XH
+  | S x -> succ (of_succ_nat x)
  end
 
 module Coq_Pos =
@@ -248,20 +356,6 @@ module Coq_Pos =
     | XO p -> XO (mul p y)
     | XH -> y
 
-  (** val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1 **)
-
-  let rec iter f x = function
-  | XI n' -> f (iter f (iter f x n') n')
-  | XO n' -> iter f (iter f x n') n'
-  | XH -> f x
-
-  (** val size_nat : positive -> nat **)
-
-  let rec size_nat = function
-  | XI p2 -> S (size_nat p2)
-  | XO p2 -> S (size_nat p2)
-  | XH -> S O
-
   (** val compare_cont : comparison -> positive -> positive -> comparison **)
 
   let rec compare_cont r x y =
@@ -285,27 +379,6 @@ module Coq_Pos =
   let compare =
     compare_cont Eq
 
-  (** val max : positive -> positive -> positive **)
-
-  let max p p' =
-    match compare p p' with
-    | Gt -> p
-    | _ -> p'
-
-  (** val eqb : positive -> positive -> bool **)
-
-  let rec eqb p q0 =
-    match p with
-    | XI p2 -> (match q0 with
-                | XI q1 -> eqb p2 q1
-                | _ -> false)
-    | XO p2 -> (match q0 with
-                | XO q1 -> eqb p2 q1
-                | _ -> false)
-    | XH -> (match q0 with
-             | XH -> true
-             | _ -> false)
-
   (** val leb : positive -> positive -> bool **)
 
   let leb x y =
@@ -313,6 +386,20 @@ module Coq_Pos =
     | Gt -> false
     | _ -> true
 
+  (** val size_nat : positive -> nat **)
+
+  let rec size_nat = function
+  | XI p2 -> S (size_nat p2)
+  | XO p2 -> S (size_nat p2)
+  | XH -> S O
+
+  (** val max : positive -> positive -> positive **)
+
+  let max p p' =
+    match compare p p' with
+    | Gt -> p
+    | _ -> p'
+
   (** val gcdn : nat -> positive -> positive -> positive **)
 
   let rec gcdn n0 a b =
@@ -340,12 +427,6 @@ module Coq_Pos =
 
   let gcd a b =
     gcdn (Coq__1.add (size_nat a) (size_nat b)) a b
-
-  (** val of_succ_nat : nat -> positive **)
-
-  let rec of_succ_nat = function
-  | O -> XH
-  | S x -> succ (of_succ_nat x)
  end
 
 module N =
@@ -354,7 +435,7 @@ module N =
 
   let of_nat = function
   | O -> N0
-  | S n' -> Npos (Coq_Pos.of_succ_nat n')
+  | S n' -> Npos (Pos.of_succ_nat n')
  end
 
 (** val pow_pos : ('a1 -> 'a1 -> 'a1) -> 'a1 -> positive -> 'a1 **)
@@ -378,13 +459,13 @@ module Z =
   let succ_double = function
   | Z0 -> Zpos XH
   | Zpos p -> Zpos (XI p)
-  | Zneg p -> Zneg (Coq_Pos.pred_double p)
+  | Zneg p -> Zneg (Pos.pred_double p)
 
   (** val pred_double : z -> z **)
 
   let pred_double = function
   | Z0 -> Zneg XH
-  | Zpos p -> Zpos (Coq_Pos.pred_double p)
+  | Zpos p -> Zpos (Pos.pred_double p)
   | Zneg p -> Zneg (XI p)
 
   (** val pos_sub : positive -> positive -> z **)
@@ -400,11 +481,11 @@ module Z =
       (match y with
        | XI q0 -> pred_double (pos_sub p q0)
        | XO q0 -> double (pos_sub p q0)
-       | XH -> Zpos (Coq_Pos.pred_double p))
+       | XH -> Zpos (Pos.pred_double p))
     | XH ->
       (match y with
        | XI q0 -> Zneg (XO q0)
-       | XO q0 -> Zneg (Coq_Pos.pred_double q0)
+       | XO q0 -> Zneg (Pos.pred_double q0)
        | XH -> Z0)
 
   (** val add : z -> z -> z **)
@@ -415,13 +496,13 @@ module Z =
     | Zpos x' ->
       (match y with
        | Z0 -> x
-       | Zpos y' -> Zpos (Coq_Pos.add x' y')
+       | Zpos y' -> Zpos (Pos.add x' y')
        | Zneg y' -> pos_sub x' y')
     | Zneg x' ->
       (match y with
        | Z0 -> x
        | Zpos y' -> pos_sub y' x'
-       | Zneg y' -> Zneg (Coq_Pos.add x' y'))
+       | Zneg y' -> Zneg (Pos.add x' y'))
 
   (** val opp : z -> z **)
 
@@ -443,18 +524,18 @@ module Z =
     | Zpos x' ->
       (match y with
        | Z0 -> Z0
-       | Zpos y' -> Zpos (Coq_Pos.mul x' y')
-       | Zneg y' -> Zneg (Coq_Pos.mul x' y'))
+       | Zpos y' -> Zpos (Pos.mul x' y')
+       | Zneg y' -> Zneg (Pos.mul x' y'))
     | Zneg x' ->
       (match y with
        | Z0 -> Z0
-       | Zpos y' -> Zneg (Coq_Pos.mul x' y')
-       | Zneg y' -> Zpos (Coq_Pos.mul x' y'))
+       | Zpos y' -> Zneg (Pos.mul x' y')
+       | Zneg y' -> Zpos (Pos.mul x' y'))
 
   (** val pow_pos : z -> positive -> z **)
 
   let pow_pos z0 =
-    Coq_Pos.iter (mul z0) (Zpos XH)
+    Pos.iter (mul z0) (Zpos XH)
 
   (** val pow : z -> z -> z **)
 
@@ -472,11 +553,11 @@ module Z =
              | Zpos _ -> Lt
              | Zneg _ -> Gt)
     | Zpos x' -> (match y with
-                  | Zpos y' -> Coq_Pos.compare x' y'
+                  | Zpos y' -> Pos.compare x' y'
                   | _ -> Gt)
     | Zneg x' ->
       (match y with
-       | Zneg y' -> compOpp (Coq_Pos.compare x' y')
+       | Zneg y' -> compOpp (Pos.compare x' y')
        | _ -> Lt)
 
   (** val leb : z -> z -> bool **)
@@ -493,13 +574,6 @@ module Z =
     | Lt -> true
     | _ -> false
 
-  (** val gtb : z -> z -> bool **)
-
-  let gtb x y =
-    match compare x y with
-    | Gt -> true
-    | _ -> false
-
   (** val eqb : z -> z -> bool **)
 
   let eqb x y =
@@ -508,10 +582,10 @@ module Z =
              | Z0 -> true
              | _ -> false)
     | Zpos p -> (match y with
-                 | Zpos q0 -> Coq_Pos.eqb p q0
+                 | Zpos q0 -> Pos.eqb p q0
                  | _ -> false)
     | Zneg p -> (match y with
-                 | Zneg q0 -> Coq_Pos.eqb p q0
+                 | Zneg q0 -> Pos.eqb p q0
                  | _ -> false)
 
   (** val max : z -> z -> z **)
@@ -521,23 +595,11 @@ module Z =
     | Lt -> m
     | _ -> n0
 
-  (** val abs : z -> z **)
-
-  let abs = function
-  | Zneg p -> Zpos p
-  | x -> x
-
-  (** val to_N : z -> n **)
-
-  let to_N = function
-  | Zpos p -> Npos p
-  | _ -> N0
-
   (** val of_nat : nat -> z **)
 
   let of_nat = function
   | O -> Z0
-  | S n1 -> Zpos (Coq_Pos.of_succ_nat n1)
+  | S n1 -> Zpos (Pos.of_succ_nat n1)
 
   (** val of_N : n -> z **)
 
@@ -592,6 +654,25 @@ module Z =
   let div a b =
     let q0,_ = div_eucl a b in q0
 
+  (** val gtb : z -> z -> bool **)
+
+  let gtb x y =
+    match compare x y with
+    | Gt -> true
+    | _ -> false
+
+  (** val abs : z -> z **)
+
+  let abs = function
+  | Zneg p -> Zpos p
+  | x -> x
+
+  (** val to_N : z -> n **)
+
+  let to_N = function
+  | Zpos p -> Npos p
+  | _ -> N0
+
   (** val gcd : z -> z -> z **)
 
   let gcd a b =
@@ -607,6 +688,11 @@ module Z =
        | Z0 -> abs a
        | Zpos b0 -> Zpos (Coq_Pos.gcd a0 b0)
        | Zneg b0 -> Zpos (Coq_Pos.gcd a0 b0))
+
+  (** val lcm : z -> z -> z **)
+
+  let lcm a b =
+    abs (mul a (div b (gcd a b)))
  end
 
 type 'c pExpr =
@@ -1083,7 +1169,7 @@ let rec map_bformula _ fct = function
 | TT k -> TT k
 | FF k -> FF k
 | X (k, p) -> X (k, p)
-| A (k, a, t0) -> A (k, (fct a), t0)
+| A (k, a, t1) -> A (k, (fct a), t1)
 | AND (k0, f1, f2) ->
   AND (k0, (map_bformula k0 fct f1), (map_bformula k0 fct f2))
 | OR (k0, f1, f2) ->
@@ -1114,21 +1200,21 @@ let cnf_ff =
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2)
     clause -> ('a1, 'a2) clause option **)
 
-let rec add_term unsat deduce t0 = function
+let rec add_term unsat deduce t1 = function
 | [] ->
-  (match deduce (fst t0) (fst t0) with
-   | Some u -> if unsat u then None else Some (t0::[])
-   | None -> Some (t0::[]))
+  (match deduce (fst t1) (fst t1) with
+   | Some u -> if unsat u then None else Some (t1::[])
+   | None -> Some (t1::[]))
 | t'::cl0 ->
-  (match deduce (fst t0) (fst t') with
+  (match deduce (fst t1) (fst t') with
    | Some u ->
      if unsat u
      then None
-     else (match add_term unsat deduce t0 cl0 with
+     else (match add_term unsat deduce t1 cl0 with
            | Some cl' -> Some (t'::cl')
            | None -> None)
    | None ->
-     (match add_term unsat deduce t0 cl0 with
+     (match add_term unsat deduce t1 cl0 with
       | Some cl' -> Some (t'::cl')
       | None -> None))
 
@@ -1139,8 +1225,8 @@ let rec add_term unsat deduce t0 = function
 let rec or_clause unsat deduce cl1 cl2 =
   match cl1 with
   | [] -> Some cl2
-  | t0::cl ->
-    (match add_term unsat deduce t0 cl2 with
+  | t1::cl ->
+    (match add_term unsat deduce t1 cl2 with
      | Some cl' -> or_clause unsat deduce cl cl'
      | None -> None)
 
@@ -1148,9 +1234,9 @@ let rec or_clause unsat deduce cl1 cl2 =
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1,
     'a2) cnf -> ('a1, 'a2) cnf **)
 
-let xor_clause_cnf unsat deduce t0 f =
+let xor_clause_cnf unsat deduce t1 f =
   fold_left (fun acc e ->
-    match or_clause unsat deduce t0 e with
+    match or_clause unsat deduce t1 e with
     | Some cl -> cl::acc
     | None -> acc) f []
 
@@ -1158,10 +1244,10 @@ let xor_clause_cnf unsat deduce t0 f =
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause -> ('a1,
     'a2) cnf -> ('a1, 'a2) cnf **)
 
-let or_clause_cnf unsat deduce t0 f =
-  match t0 with
+let or_clause_cnf unsat deduce t1 f =
+  match t1 with
   | [] -> f
-  | _::_ -> xor_clause_cnf unsat deduce t0 f
+  | _::_ -> xor_clause_cnf unsat deduce t1 f
 
 (** val or_cnf :
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1,
@@ -1269,7 +1355,7 @@ let rec xcnf unsat deduce normalise1 negate0 pol0 _ = function
 | TT _ -> if pol0 then cnf_tt else cnf_ff
 | FF _ -> if pol0 then cnf_ff else cnf_tt
 | X (_, _) -> cnf_ff
-| A (_, x, t0) -> if pol0 then normalise1 x t0 else negate0 x t0
+| A (_, x, t1) -> if pol0 then normalise1 x t1 else negate0 x t1
 | AND (k0, e1, e2) ->
   mk_and unsat deduce (fun x x0 x1 ->
     xcnf unsat deduce normalise1 negate0 x x0 x1) k0 pol0 e1 e2
@@ -1301,21 +1387,21 @@ let rec xcnf unsat deduce normalise1 negate0 pol0 _ = function
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2)
     clause -> (('a1, 'a2) clause, 'a2 trace) sum **)
 
-let rec radd_term unsat deduce t0 = function
+let rec radd_term unsat deduce t1 = function
 | [] ->
-  (match deduce (fst t0) (fst t0) with
-   | Some u -> if unsat u then Inr (Push ((snd t0), Null)) else Inl (t0::[])
-   | None -> Inl (t0::[]))
+  (match deduce (fst t1) (fst t1) with
+   | Some u -> if unsat u then Inr (Push ((snd t1), Null)) else Inl (t1::[])
+   | None -> Inl (t1::[]))
 | t'::cl0 ->
-  (match deduce (fst t0) (fst t') with
+  (match deduce (fst t1) (fst t') with
    | Some u ->
      if unsat u
-     then Inr (Push ((snd t0), (Push ((snd t'), Null))))
-     else (match radd_term unsat deduce t0 cl0 with
+     then Inr (Push ((snd t1), (Push ((snd t'), Null))))
+     else (match radd_term unsat deduce t1 cl0 with
            | Inl cl' -> Inl (t'::cl')
            | Inr l -> Inr l)
    | None ->
-     (match radd_term unsat deduce t0 cl0 with
+     (match radd_term unsat deduce t1 cl0 with
       | Inl cl' -> Inl (t'::cl')
       | Inr l -> Inr l))
 
@@ -1326,8 +1412,8 @@ let rec radd_term unsat deduce t0 = function
 let rec ror_clause unsat deduce cl1 cl2 =
   match cl1 with
   | [] -> Inl cl2
-  | t0::cl ->
-    (match radd_term unsat deduce t0 cl2 with
+  | t1::cl ->
+    (match radd_term unsat deduce t1 cl2 with
      | Inl cl' -> ror_clause unsat deduce cl cl'
      | Inr l -> Inr l)
 
@@ -1335,10 +1421,10 @@ let rec ror_clause unsat deduce cl1 cl2 =
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1,
     'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace **)
 
-let xror_clause_cnf unsat deduce t0 f =
+let xror_clause_cnf unsat deduce t1 f =
   fold_left (fun pat e ->
     let acc,tg = pat in
-    (match ror_clause unsat deduce t0 e with
+    (match ror_clause unsat deduce t1 e with
      | Inl cl -> (cl::acc),tg
      | Inr l -> acc,(Merge (tg, l))))
     f ([],Null)
@@ -1347,10 +1433,10 @@ let xror_clause_cnf unsat deduce t0 f =
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1,
     'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace **)
 
-let ror_clause_cnf unsat deduce t0 f =
-  match t0 with
+let ror_clause_cnf unsat deduce t1 f =
+  match t1 with
   | [] -> f,Null
-  | _::_ -> xror_clause_cnf unsat deduce t0 f
+  | _::_ -> xror_clause_cnf unsat deduce t1 f
 
 (** val ror_cnf :
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause list ->
@@ -1360,9 +1446,9 @@ let rec ror_cnf unsat deduce f f' =
   match f with
   | [] -> cnf_tt,Null
   | e::rst ->
-    let rst_f',t0 = ror_cnf unsat deduce rst f' in
+    let rst_f',t1 = ror_cnf unsat deduce rst f' in
     let e_f',t' = ror_clause_cnf unsat deduce e f' in
-    (rev_append rst_f' e_f'),(Merge (t0, t'))
+    (rev_append rst_f' e_f'),(Merge (t1, t'))
 
 (** val ror_cnf_opt :
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1,
@@ -1452,8 +1538,8 @@ let rec rxcnf unsat deduce normalise1 negate0 polarity _ = function
 | TT _ -> if polarity then cnf_tt,Null else cnf_ff,Null
 | FF _ -> if polarity then cnf_ff,Null else cnf_tt,Null
 | X (_, _) -> cnf_ff,Null
-| A (_, x, t0) ->
-  ratom (if polarity then normalise1 x t0 else negate0 x t0) t0
+| A (_, x, t1) ->
+  ratom (if polarity then normalise1 x t1 else negate0 x t1) t1
 | AND (k0, e1, e2) ->
   rxcnf_and unsat deduce (fun x x0 x1 ->
     rxcnf unsat deduce normalise1 negate0 x x0 x1) polarity k0 e1 e2
@@ -1489,7 +1575,7 @@ let rec aformula to_constr _ = function
 | TT b -> to_constr.mkTT b
 | FF b -> to_constr.mkFF b
 | X (_, p) -> p
-| A (b, x, t0) -> to_constr.mkA b x t0
+| A (b, x, t1) -> to_constr.mkA b x t1
 | AND (k0, f1, f2) ->
   to_constr.mkAND k0 (aformula to_constr k0 f1) (aformula to_constr k0 f2)
 | OR (k0, f1, f2) ->
@@ -1563,8 +1649,8 @@ let mk_arrow o k f1 f2 =
     'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula **)
 
 let rec abst_simpl to_constr needA _ = function
-| A (k, x, t0) ->
-  if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0))
+| A (k, x, t1) ->
+  if needA t1 then A (k, x, t1) else X (k, (to_constr.mkA k x t1))
 | AND (k0, f1, f2) ->
   AND (k0, (abst_simpl to_constr needA k0 f1),
     (abst_simpl to_constr needA k0 f2))
@@ -1673,8 +1759,8 @@ let rec abst_form to_constr needA pol0 _ = function
 | TT k -> if pol0 then TT k else X (k, (to_constr.mkTT k))
 | FF k -> if pol0 then X (k, (to_constr.mkFF k)) else FF k
 | X (k, p) -> X (k, p)
-| A (k, x, t0) ->
-  if needA t0 then A (k, x, t0) else X (k, (to_constr.mkA k x t0))
+| A (k, x, t1) ->
+  if needA t1 then A (k, x, t1) else X (k, (to_constr.mkA k x t1))
 | AND (k0, f1, f2) ->
   abst_and to_constr (abst_form to_constr needA) pol0 k0 f1 f2
 | OR (k0, f1, f2) ->
@@ -1955,8 +2041,8 @@ let cnf_of_list cO ceqb cleb l tg =
     -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool)
     -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf **)
 
-let cnf_normalise cO cI cplus ctimes cminus copp ceqb cleb t0 tg =
-  let f = normalise cO cI cplus ctimes cminus copp ceqb t0 in
+let cnf_normalise cO cI cplus ctimes cminus copp ceqb cleb t1 tg =
+  let f = normalise cO cI cplus ctimes cminus copp ceqb t1 in
   if check_inconsistent cO ceqb cleb f
   then cnf_ff
   else cnf_of_list cO ceqb cleb (xnormalise copp f) tg
@@ -1966,8 +2052,8 @@ let cnf_normalise cO cI cplus ctimes cminus copp ceqb cleb t0 tg =
     -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool)
     -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf **)
 
-let cnf_negate cO cI cplus ctimes cminus copp ceqb cleb t0 tg =
-  let f = normalise cO cI cplus ctimes cminus copp ceqb t0 in
+let cnf_negate cO cI cplus ctimes cminus copp ceqb cleb t1 tg =
+  let f = normalise cO cI cplus ctimes cminus copp ceqb t1 in
   if check_inconsistent cO ceqb cleb f
   then cnf_tt
   else cnf_of_list cO ceqb cleb (xnegate copp f) tg
@@ -2008,10 +2094,10 @@ let map_Formula c_of_S f =
     'a1 psatz **)
 
 let simpl_cone cO cI ctimes ceqb e = match e with
-| PsatzSquare t0 ->
-  (match t0 with
+| PsatzSquare t1 ->
+  (match t1 with
    | Pc c -> if ceqb cO c then PsatzZ else PsatzC (ctimes c c)
-   | _ -> PsatzSquare t0)
+   | _ -> PsatzSquare t1)
 | PsatzMulE (t1, t2) ->
   (match t1 with
    | PsatzMulE (x, x0) ->
@@ -2061,65 +2147,50 @@ let simpl_cone cO cI ctimes ceqb e = match e with
            | _ -> PsatzAdd (t1, t2)))
 | _ -> e
 
-type q = { qnum : z; qden : positive }
-
-(** val qeq_bool : q -> q -> bool **)
-
-let qeq_bool x y =
-  Z.eqb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
-
-(** val qle_bool : q -> q -> bool **)
-
-let qle_bool x y =
-  Z.leb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
-
-(** val qplus : q -> q -> q **)
-
-let qplus x y =
-  { qnum = (Z.add (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)));
-    qden = (Coq_Pos.mul x.qden y.qden) }
-
-(** val qmult : q -> q -> q **)
-
-let qmult x y =
-  { qnum = (Z.mul x.qnum y.qnum); qden = (Coq_Pos.mul x.qden y.qden) }
-
-(** val qopp : q -> q **)
-
-let qopp x =
-  { qnum = (Z.opp x.qnum); qden = x.qden }
-
-(** val qminus : q -> q -> q **)
-
-let qminus x y =
-  qplus x (qopp y)
-
-(** val qinv : q -> q **)
-
-let qinv x =
-  match x.qnum with
-  | Z0 -> { qnum = Z0; qden = XH }
-  | Zpos p -> { qnum = (Zpos x.qden); qden = p }
-  | Zneg p -> { qnum = (Zneg x.qden); qden = p }
-
-(** val qpower_positive : q -> positive -> q **)
-
-let qpower_positive =
-  pow_pos qmult
-
-(** val qpower : q -> z -> q **)
-
-let qpower q0 = function
-| Z0 -> { qnum = (Zpos XH); qden = XH }
-| Zpos p -> qpower_positive q0 p
-| Zneg p -> qinv (qpower_positive q0 p)
+module PositiveSet =
+ struct
+  type tree =
+  | Leaf
+  | Node of tree * bool * tree
+
+  type t = tree
+
+  (** val empty : t **)
+
+  let empty =
+    Leaf
+
+  (** val mem : positive -> t -> bool **)
+
+  let rec mem i = function
+  | Leaf -> false
+  | Node (l, o, r) ->
+    (match i with
+     | XI i0 -> mem i0 r
+     | XO i0 -> mem i0 l
+     | XH -> o)
+
+  (** val add : positive -> t -> t **)
+
+  let rec add i = function
+  | Leaf ->
+    (match i with
+     | XI i0 -> Node (Leaf, false, (add i0 Leaf))
+     | XO i0 -> Node ((add i0 Leaf), false, Leaf)
+     | XH -> Node (Leaf, true, Leaf))
+  | Node (l, o, r) ->
+    (match i with
+     | XI i0 -> Node (l, o, (add i0 r))
+     | XO i0 -> Node ((add i0 l), o, r)
+     | XH -> Node (l, true, r))
+ end
 
-type 'a t =
+type 'a t0 =
 | Empty
 | Elt of 'a
-| Branch of 'a t * 'a * 'a t
+| Branch of 'a t0 * 'a * 'a t0
 
-(** val find : 'a1 -> 'a1 t -> positive -> 'a1 **)
+(** val find : 'a1 -> 'a1 t0 -> positive -> 'a1 **)
 
 let rec find default vm p =
   match vm with
@@ -2131,7 +2202,7 @@ let rec find default vm p =
      | XO p2 -> find default l p2
      | XH -> e)
 
-(** val singleton : 'a1 -> positive -> 'a1 -> 'a1 t **)
+(** val singleton : 'a1 -> positive -> 'a1 -> 'a1 t0 **)
 
 let rec singleton default x v =
   match x with
@@ -2139,7 +2210,7 @@ let rec singleton default x v =
   | XO p -> Branch ((singleton default p v), default, Empty)
   | XH -> Elt v
 
-(** val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t **)
+(** val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t0 -> 'a1 t0 **)
 
 let rec vm_add default x v = function
 | Empty -> singleton default x v
@@ -2154,28 +2225,6 @@ let rec vm_add default x v = function
    | XO p -> Branch ((vm_add default p v l), o, r)
    | XH -> Branch (l, v, r))
 
-(** val zeval_const : z pExpr -> z option **)
-
-let rec zeval_const = function
-| PEc c -> Some c
-| PEX _ -> None
-| PEadd (e1, e2) ->
-  map_option2 (fun x y -> Some (Z.add x y)) (zeval_const e1) (zeval_const e2)
-| PEsub (e1, e2) ->
-  map_option2 (fun x y -> Some (Z.sub x y)) (zeval_const e1) (zeval_const e2)
-| PEmul (e1, e2) ->
-  map_option2 (fun x y -> Some (Z.mul x y)) (zeval_const e1) (zeval_const e2)
-| PEopp e0 -> map_option (fun x -> Some (Z.opp x)) (zeval_const e0)
-| PEpow (e1, n0) ->
-  map_option (fun x -> Some (Z.pow x (Z.of_N n0))) (zeval_const e1)
-
-type zWitness = z psatz
-
-(** val zWeakChecker : z nFormula list -> z psatz -> bool **)
-
-let zWeakChecker =
-  check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul Z.eqb Z.leb
-
 (** val psub1 : z pol -> z pol -> z pol **)
 
 let psub1 =
@@ -2191,9 +2240,9 @@ let popp1 =
 let padd1 =
   padd0 Z0 Z.add Z.eqb
 
-(** val normZ : z pExpr -> z pol **)
+(** val norm0 : z pExpr -> z pol **)
 
-let normZ =
+let norm0 =
   norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp Z.eqb
 
 (** val zunsat : z nFormula -> bool **)
@@ -2208,10 +2257,10 @@ let zdeduce =
 
 (** val xnnormalise : z formula -> z nFormula **)
 
-let xnnormalise t0 =
-  let { flhs = lhs; fop = o; frhs = rhs } = t0 in
-  let lhs0 = normZ lhs in
-  let rhs0 = normZ rhs in
+let xnnormalise t1 =
+  let { flhs = lhs; fop = o; frhs = rhs } = t1 in
+  let lhs0 = norm0 lhs in
+  let rhs0 = norm0 rhs in
   (match o with
    | OpEq -> (psub1 rhs0 lhs0),Equal
    | OpNEq -> (psub1 rhs0 lhs0),NonEqual
@@ -2220,52 +2269,33 @@ let xnnormalise t0 =
    | OpLt -> (psub1 rhs0 lhs0),Strict
    | OpGt -> (psub1 lhs0 rhs0),Strict)
 
-(** val xnormalise0 : z nFormula -> z nFormula list **)
-
-let xnormalise0 = function
-| e,o ->
-  (match o with
-   | Equal ->
-     ((psub1 e (Pc (Zpos XH))),NonStrict)::(((psub1 (Pc (Zneg XH)) e),NonStrict)::[])
-   | NonEqual -> (e,Equal)::[]
-   | Strict -> ((psub1 (Pc Z0) e),NonStrict)::[]
-   | NonStrict -> ((psub1 (Pc (Zneg XH)) e),NonStrict)::[])
-
-(** val cnf_of_list0 :
-    'a1 -> z nFormula list -> (z nFormula * 'a1) list list **)
-
-let cnf_of_list0 tg l =
-  fold_right (fun x acc -> if zunsat x then acc else ((x,tg)::[])::acc)
-    cnf_tt l
+(** val xis_integral : (positive -> bool) -> positive -> z pol -> bool **)
 
-(** val normalise0 : z formula -> 'a1 -> (z nFormula, 'a1) cnf **)
+let rec xis_integral e jmp = function
+| Pc _ -> true
+| Pinj (j, p2) -> xis_integral e (Coq_Pos.add j jmp) p2
+| PX (p2, _, q0) ->
+  (&&) ((&&) (xis_integral e jmp p2) (e jmp))
+    (xis_integral e (Coq_Pos.succ jmp) q0)
 
-let normalise0 t0 tg =
-  let f = xnnormalise t0 in
-  if zunsat f then cnf_ff else cnf_of_list0 tg (xnormalise0 f)
+(** val get : PositiveSet.t -> positive -> bool **)
 
-(** val xnegate0 : z nFormula -> z nFormula list **)
+let get s x =
+  PositiveSet.mem x s
 
-let xnegate0 = function
-| e,o ->
-  (match o with
-   | NonEqual ->
-     ((psub1 e (Pc (Zpos XH))),NonStrict)::(((psub1 (Pc (Zneg XH)) e),NonStrict)::[])
-   | Strict -> ((psub1 e (Pc (Zpos XH))),NonStrict)::[]
-   | x -> (e,x)::[])
+(** val oget : PositiveSet.t option -> positive -> bool **)
 
-(** val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf **)
+let oget s x =
+  match s with
+  | Some s0 -> PositiveSet.mem x s0
+  | None -> true
 
-let negate t0 tg =
-  let f = xnnormalise t0 in
-  if zunsat f then cnf_tt else cnf_of_list0 tg (xnegate0 f)
-
-(** val cnfZ :
-    kind -> (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1)
-    cnf * 'a1 trace **)
+(** val is_integral : PositiveSet.t option -> z pol -> bool **)
 
-let cnfZ k f =
-  rxcnf zunsat zdeduce normalise0 negate true k f
+let is_integral e pol0 =
+  match e with
+  | Some e0 -> xis_integral (get e0) XH pol0
+  | None -> true
 
 (** val ceiling : z -> z -> z **)
 
@@ -2275,6 +2305,8 @@ let ceiling a b =
    | Z0 -> q0
    | _ -> Z.add q0 (Zpos XH))
 
+type zWitness = z psatz
+
 type zArithProof =
 | DoneProof
 | RatProof of zWitness * zArithProof
@@ -2349,9 +2381,8 @@ let eval_Psatz0 =
 (** val valid_cut_sign : op1 -> bool **)
 
 let valid_cut_sign = function
-| Equal -> true
-| NonStrict -> true
-| _ -> false
+| NonEqual -> false
+| _ -> true
 
 (** val bound_var : positive -> z formula **)
 
@@ -2360,8 +2391,8 @@ let bound_var v =
 
 (** val mk_eq_pos : positive -> positive -> positive -> z formula **)
 
-let mk_eq_pos x y t0 =
-  { flhs = (PEX x); fop = OpEq; frhs = (PEsub ((PEX y), (PEX t0))) }
+let mk_eq_pos x y t1 =
+  { flhs = (PEX x); fop = OpEq; frhs = (PEsub ((PEX y), (PEX t1))) }
 
 (** val max_var : positive -> z pol -> positive **)
 
@@ -2376,73 +2407,217 @@ let rec max_var jmp = function
 let max_var_nformulae l =
   fold_left (fun acc f -> Coq_Pos.max acc (max_var XH (fst f))) l XH
 
-(** val zChecker : z nFormula list -> zArithProof -> bool **)
+(** val add0 : positive -> PositiveSet.t option -> PositiveSet.t option **)
+
+let add0 x = function
+| Some s0 -> Some (PositiveSet.add x s0)
+| None -> None
 
-let rec zChecker l = function
+(** val zChecker :
+    PositiveSet.t option -> z nFormula list -> zArithProof -> bool **)
+
+let rec zChecker is_integer l = function
 | DoneProof -> false
 | RatProof (w, pf0) ->
   (match eval_Psatz0 l w with
-   | Some f -> if zunsat f then true else zChecker (f::l) pf0
+   | Some f -> if zunsat f then true else zChecker is_integer (f::l) pf0
    | None -> false)
 | CutProof (w, pf0) ->
   (match eval_Psatz0 l w with
    | Some f ->
-     (match genCuttingPlane f with
-      | Some cp -> zChecker ((nformula_of_cutting_plane cp)::l) pf0
-      | None -> true)
+     if is_integral is_integer (fst f)
+     then (match genCuttingPlane f with
+           | Some cp ->
+             let f0 = nformula_of_cutting_plane cp in
+             if zunsat f0 then true else zChecker is_integer (f0::l) pf0
+           | None -> true)
+     else false
    | None -> false)
 | SplitProof (p, pf1, pf2) ->
-  (match genCuttingPlane (p,NonStrict) with
-   | Some cp1 ->
-     (match genCuttingPlane ((popp1 p),NonStrict) with
-      | Some cp2 ->
-        (&&) (zChecker ((nformula_of_cutting_plane cp1)::l) pf1)
-          (zChecker ((nformula_of_cutting_plane cp2)::l) pf2)
-      | None -> false)
-   | None -> false)
+  if is_integral is_integer p
+  then (match genCuttingPlane (p,NonStrict) with
+        | Some cp1 ->
+          (match genCuttingPlane ((popp1 p),NonStrict) with
+           | Some cp2 ->
+             (&&)
+               (zChecker is_integer ((nformula_of_cutting_plane cp1)::l) pf1)
+               (zChecker is_integer ((nformula_of_cutting_plane cp2)::l) pf2)
+           | None -> false)
+        | None -> false)
+  else false
 | EnumProof (w1, w2, pf0) ->
   (match eval_Psatz0 l w1 with
    | Some f1 ->
      (match eval_Psatz0 l w2 with
       | Some f2 ->
-        (match genCuttingPlane f1 with
-         | Some p ->
-           let p2,op3 = p in
-           let e1,z1 = p2 in
-           (match genCuttingPlane f2 with
-            | Some p3 ->
-              let p4,op4 = p3 in
-              let e2,z2 = p4 in
-              if (&&) ((&&) (valid_cut_sign op3) (valid_cut_sign op4))
-                   (is_pol_Z0 (padd1 e1 e2))
-              then let rec label pfs lb ub =
-                     match pfs with
-                     | [] -> Z.gtb lb ub
-                     | pf1::rsr ->
-                       (&&) (zChecker (((psub1 e1 (Pc lb)),Equal)::l) pf1)
-                         (label rsr (Z.add lb (Zpos XH)) ub)
-                   in label pf0 (Z.opp z1) z2
-              else false
-            | None -> true)
-         | None -> true)
+        if (&&) (is_integral is_integer (fst f1))
+             (is_integral is_integer (fst f2))
+        then (match genCuttingPlane f1 with
+              | Some p ->
+                let p2,op3 = p in
+                let e1,z1 = p2 in
+                (match genCuttingPlane f2 with
+                 | Some p3 ->
+                   let p4,op4 = p3 in
+                   let e2,z2 = p4 in
+                   if (&&) ((&&) (valid_cut_sign op3) (valid_cut_sign op4))
+                        (is_pol_Z0 (padd1 e1 e2))
+                   then let rec label pfs lb ub =
+                          match pfs with
+                          | [] -> Z.gtb lb ub
+                          | pf1::rsr ->
+                            (&&)
+                              (zChecker is_integer
+                                (((psub1 e1 (Pc lb)),Equal)::l) pf1)
+                              (label rsr (Z.add lb (Zpos XH)) ub)
+                        in label pf0 (Z.opp z1) z2
+                   else false
+                 | None -> true)
+              | None -> true)
+        else false
       | None -> false)
    | None -> false)
 | ExProof (x, prf) ->
   let fr = max_var_nformulae l in
-  if Coq_Pos.leb x fr
+  if (&&) (Coq_Pos.leb x fr) (oget is_integer x)
   then let z0 = Coq_Pos.succ fr in
-       let t0 = Coq_Pos.succ z0 in
-       let nfx = xnnormalise (mk_eq_pos x z0 t0) in
+       let t1 = Coq_Pos.succ z0 in
+       let nfx = xnnormalise (mk_eq_pos x z0 t1) in
        let posz = xnnormalise (bound_var z0) in
-       let post = xnnormalise (bound_var t0) in
-       zChecker (nfx::(posz::(post::l))) prf
+       let post = xnnormalise (bound_var t1) in
+       zChecker (add0 z0 (add0 t1 is_integer)) (nfx::(posz::(post::l))) prf
   else false
 
+(** val zeval_const : z pExpr -> z option **)
+
+let rec zeval_const = function
+| PEc c -> Some c
+| PEX _ -> None
+| PEadd (e1, e2) ->
+  map_option2 (fun x y -> Some (Z.add x y)) (zeval_const e1) (zeval_const e2)
+| PEsub (e1, e2) ->
+  map_option2 (fun x y -> Some (Z.sub x y)) (zeval_const e1) (zeval_const e2)
+| PEmul (e1, e2) ->
+  map_option2 (fun x y -> Some (Z.mul x y)) (zeval_const e1) (zeval_const e2)
+| PEopp e0 -> map_option (fun x -> Some (Z.opp x)) (zeval_const e0)
+| PEpow (e1, n0) ->
+  map_option (fun x -> Some (Z.pow x (Z.of_N n0))) (zeval_const e1)
+
+(** val zWeakChecker : z nFormula list -> z psatz -> bool **)
+
+let zWeakChecker =
+  check_normalised_formulas Z0 (Zpos XH) Z.add Z.mul Z.eqb Z.leb
+
+(** val normZ : z pExpr -> z pol **)
+
+let normZ =
+  norm Z0 (Zpos XH) Z.add Z.mul Z.sub Z.opp Z.eqb
+
+(** val cnf_of_list0 :
+    'a1 -> z nFormula list -> (z nFormula * 'a1) list list **)
+
+let cnf_of_list0 tg l =
+  fold_right (fun x acc -> if zunsat x then acc else ((x,tg)::[])::acc)
+    cnf_tt l
+
+(** val xnormalise0 : z nFormula -> z nFormula list **)
+
+let xnormalise0 = function
+| e,o ->
+  (match o with
+   | Equal ->
+     ((psub1 e (Pc (Zpos XH))),NonStrict)::(((psub1 (Pc (Zneg XH)) e),NonStrict)::[])
+   | NonEqual -> (e,Equal)::[]
+   | Strict -> ((psub1 (Pc Z0) e),NonStrict)::[]
+   | NonStrict -> ((psub1 (Pc (Zneg XH)) e),NonStrict)::[])
+
+(** val normalise0 : z formula -> 'a1 -> (z nFormula, 'a1) cnf **)
+
+let normalise0 t1 tg =
+  let f = xnnormalise t1 in
+  if zunsat f then cnf_ff else cnf_of_list0 tg (xnormalise0 f)
+
+(** val xnegate0 : z nFormula -> z nFormula list **)
+
+let xnegate0 = function
+| e,o ->
+  (match o with
+   | NonEqual ->
+     ((psub1 e (Pc (Zpos XH))),NonStrict)::(((psub1 (Pc (Zneg XH)) e),NonStrict)::[])
+   | Strict -> ((psub1 e (Pc (Zpos XH))),NonStrict)::[]
+   | x -> (e,x)::[])
+
+(** val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf **)
+
+let negate t1 tg =
+  let f = xnnormalise t1 in
+  if zunsat f then cnf_tt else cnf_of_list0 tg (xnegate0 f)
+
+(** val cnfZ :
+    kind -> (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1)
+    cnf * 'a1 trace **)
+
+let cnfZ k f =
+  rxcnf zunsat zdeduce normalise0 negate true k f
+
 (** val zTautoChecker : z formula bFormula -> zArithProof list -> bool **)
 
 let zTautoChecker f w =
   tauto_checker zunsat zdeduce normalise0 negate (fun cl ->
-    zChecker (map fst cl)) f w
+    zChecker None (map fst cl)) f w
+
+type q = { qnum : z; qden : positive }
+
+(** val qeq_bool : q -> q -> bool **)
+
+let qeq_bool x y =
+  Z.eqb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
+
+(** val qle_bool : q -> q -> bool **)
+
+let qle_bool x y =
+  Z.leb (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden))
+
+(** val qplus : q -> q -> q **)
+
+let qplus x y =
+  { qnum = (Z.add (Z.mul x.qnum (Zpos y.qden)) (Z.mul y.qnum (Zpos x.qden)));
+    qden = (Coq_Pos.mul x.qden y.qden) }
+
+(** val qmult : q -> q -> q **)
+
+let qmult x y =
+  { qnum = (Z.mul x.qnum y.qnum); qden = (Coq_Pos.mul x.qden y.qden) }
+
+(** val qopp : q -> q **)
+
+let qopp x =
+  { qnum = (Z.opp x.qnum); qden = x.qden }
+
+(** val qminus : q -> q -> q **)
+
+let qminus x y =
+  qplus x (qopp y)
+
+(** val qinv : q -> q **)
+
+let qinv x =
+  match x.qnum with
+  | Z0 -> { qnum = Z0; qden = XH }
+  | Zpos p -> { qnum = (Zpos x.qden); qden = p }
+  | Zneg p -> { qnum = (Zneg x.qden); qden = p }
+
+(** val qpower_positive : q -> positive -> q **)
+
+let qpower_positive =
+  pow_pos qmult
+
+(** val qpower : q -> z -> q **)
+
+let qpower q0 = function
+| Z0 -> { qnum = (Zpos XH); qden = XH }
+| Zpos p -> qpower_positive q0 p
+| Zneg p -> qinv (qpower_positive q0 p)
 
 type qWitness = q psatz
 
@@ -2454,15 +2629,15 @@ let qWeakChecker =
 
 (** val qnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf **)
 
-let qnormalise t0 tg =
+let qnormalise t1 tg =
   cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH }
-    qplus qmult qminus qopp qeq_bool qle_bool t0 tg
+    qplus qmult qminus qopp qeq_bool qle_bool t1 tg
 
 (** val qnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf **)
 
-let qnegate t0 tg =
+let qnegate t1 tg =
   cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus
-    qmult qminus qopp qeq_bool qle_bool t0 tg
+    qmult qminus qopp qeq_bool qle_bool t1 tg
 
 (** val qunsat : q nFormula -> bool **)
 
@@ -2525,25 +2700,19 @@ let rec q_of_Rcst = function
 | CInv r0 -> qinv (q_of_Rcst r0)
 | COpp r0 -> qopp (q_of_Rcst r0)
 
-type rWitness = q psatz
-
-(** val rWeakChecker : q nFormula list -> q psatz -> bool **)
-
-let rWeakChecker =
-  check_normalised_formulas { qnum = Z0; qden = XH } { qnum = (Zpos XH);
-    qden = XH } qplus qmult qeq_bool qle_bool
+type rWitness = zArithProof
 
 (** val rnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf **)
 
-let rnormalise t0 tg =
+let rnormalise t1 tg =
   cnf_normalise { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH }
-    qplus qmult qminus qopp qeq_bool qle_bool t0 tg
+    qplus qmult qminus qopp qeq_bool qle_bool t1 tg
 
 (** val rnegate : q formula -> 'a1 -> (q nFormula, 'a1) cnf **)
 
-let rnegate t0 tg =
+let rnegate t1 tg =
   cnf_negate { qnum = Z0; qden = XH } { qnum = (Zpos XH); qden = XH } qplus
-    qmult qminus qopp qeq_bool qle_bool t0 tg
+    qmult qminus qopp qeq_bool qle_bool t1 tg
 
 (** val runsat : q nFormula -> bool **)
 
@@ -2555,9 +2724,104 @@ let runsat =
 let rdeduce =
   nformula_plus_nformula { qnum = Z0; qden = XH } qplus qeq_bool
 
-(** val rTautoChecker : rcst formula bFormula -> rWitness list -> bool **)
+type 'form eFormula =
+| IsZ of bool * positive
+| IsF of 'form
+
+(** val map_eFormula :
+    ('a1 -> 'a2) -> 'a1 formula eFormula -> 'a2 formula eFormula **)
+
+let map_eFormula f = function
+| IsZ (b, x) -> IsZ (b, x)
+| IsF f1 -> IsF (map_Formula f f1)
+
+(** val lcm0 : q pol -> z **)
+
+let rec lcm0 = function
+| Pc q0 -> Zpos q0.qden
+| Pinj (_, p2) -> lcm0 p2
+| PX (p2, _, q0) -> Z.lcm (lcm0 p2) (lcm0 q0)
+
+(** val polZ : z -> q pol -> z pol **)
+
+let rec polZ lcm1 = function
+| Pc q0 -> Pc (Z.div (Z.mul q0.qnum lcm1) (Zpos q0.qden))
+| Pinj (x, p2) -> Pinj (x, (polZ lcm1 p2))
+| PX (p2, i, q0) -> PX ((polZ lcm1 p2), i, (polZ lcm1 q0))
+
+(** val nformulaZ : q nFormula -> z nFormula **)
+
+let nformulaZ = function
+| p,o -> (polZ (lcm0 p) p),o
+
+(** val xcollect_isZ :
+    PositiveSet.t -> z nFormula list -> (q nFormula eFormula * unit0) list ->
+    PositiveSet.t * z nFormula list **)
+
+let rec xcollect_isZ s acc = function
+| [] -> s,acc
+| p::l0 ->
+  let e,_ = p in
+  (match e with
+   | IsZ (b, x) -> xcollect_isZ (if b then PositiveSet.add x s else s) acc l0
+   | IsF f -> xcollect_isZ s ((nformulaZ f)::acc) l0)
+
+(** val qCheck : (q nFormula eFormula * unit0) list -> zArithProof -> bool **)
+
+let qCheck l =
+  let s,cl = xcollect_isZ PositiveSet.empty [] l in zChecker (Some s) cl
+
+(** val erunsat : q nFormula eFormula -> bool **)
+
+let erunsat = function
+| IsZ (_, _) -> false
+| IsF f0 -> runsat f0
+
+(** val erdeduce :
+    q nFormula eFormula -> q nFormula eFormula -> q nFormula eFormula option **)
+
+let erdeduce f1 f2 =
+  match f1 with
+  | IsZ (_, _) -> None
+  | IsF f3 ->
+    (match f2 with
+     | IsZ (_, _) -> None
+     | IsF f4 ->
+       (match rdeduce f3 f4 with
+        | Some f -> Some (IsF f)
+        | None -> None))
+
+(** val map_cnf : ('a2 -> 'a3) -> ('a2, 'a1) cnf -> ('a3, 'a1) cnf **)
+
+let map_cnf f l =
+  map (map (fun pat -> let a,t1 = pat in (f a),t1)) l
+
+(** val eRnormalise :
+    q formula eFormula -> 'a1 -> (q nFormula eFormula, 'a1) cnf **)
+
+let eRnormalise f t1 =
+  match f with
+  | IsZ (b, z0) -> (((IsZ ((negb b), z0)),t1)::[])::[]
+  | IsF f0 -> map_cnf (fun x -> IsF x) (rnormalise f0 t1)
+
+(** val eRnegate :
+    q formula eFormula -> 'a1 -> (q nFormula eFormula, 'a1) cnf **)
+
+let eRnegate f t1 =
+  match f with
+  | IsZ (b, z0) -> (((IsZ (b, z0)),t1)::[])::[]
+  | IsF f0 -> map_cnf (fun x -> IsF x) (rnegate f0 t1)
+
+(** val cnfR :
+    kind -> (q formula eFormula, 'a1, 'a2, 'a3) tFormula -> (q nFormula
+    eFormula, 'a1) cnf * 'a1 trace **)
+
+let cnfR k f =
+  rxcnf erunsat erdeduce eRnormalise eRnegate true k f
+
+(** val rTautoChecker :
+    rcst formula eFormula bFormula -> rWitness list -> bool **)
 
 let rTautoChecker f w =
-  tauto_checker runsat rdeduce rnormalise rnegate (fun cl ->
-    rWeakChecker (map fst cl))
-    (map_bformula IsProp (map_Formula q_of_Rcst) f) w
+  tauto_checker erunsat erdeduce eRnormalise eRnegate qCheck
+    (map_bformula IsProp (map_eFormula q_of_Rcst) f) w
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 7d817fbaaf0d..6d901bde2dae 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -1,6 +1,3 @@
-(* *** DO NOT EDIT *** *)
-(* This file is extracted from test-suite/output/MExtraction.v in the stdlib *)
-(* *** DO NOT EDIT *** *)
 
 type __ = Obj.t
 
@@ -32,12 +29,12 @@ val compOpp : comparison -> comparison
 
 val add : nat -> nat -> nat
 
+val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
+
 val nth : nat -> 'a1 list -> 'a1 -> 'a1
 
 val rev_append : 'a1 list -> 'a1 list -> 'a1 list
 
-val map : ('a1 -> 'a2) -> 'a1 list -> 'a2 list
-
 val fold_left : ('a1 -> 'a2 -> 'a1) -> 'a2 list -> 'a1 -> 'a1
 
 val fold_right : ('a2 -> 'a1 -> 'a1) -> 'a1 -> 'a2 list -> 'a1
@@ -58,10 +55,30 @@ type z =
 
 module Pos :
  sig
+  val succ : positive -> positive
+
+  val add : positive -> positive -> positive
+
+  val add_carry : positive -> positive -> positive
+
+  val pred_double : positive -> positive
+
   type mask =
   | IsNul
   | IsPos of positive
   | IsNeg
+
+  val mul : positive -> positive -> positive
+
+  val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1
+
+  val compare_cont : comparison -> positive -> positive -> comparison
+
+  val compare : positive -> positive -> comparison
+
+  val eqb : positive -> positive -> bool
+
+  val of_succ_nat : nat -> positive
  end
 
 module Coq_Pos :
@@ -93,23 +110,19 @@ module Coq_Pos :
 
   val mul : positive -> positive -> positive
 
-  val iter : ('a1 -> 'a1) -> 'a1 -> positive -> 'a1
-
-  val size_nat : positive -> nat
-
   val compare_cont : comparison -> positive -> positive -> comparison
 
   val compare : positive -> positive -> comparison
 
-  val max : positive -> positive -> positive
-
   val leb : positive -> positive -> bool
 
+  val size_nat : positive -> nat
+
+  val max : positive -> positive -> positive
+
   val gcdn : nat -> positive -> positive -> positive
 
   val gcd : positive -> positive -> positive
-
-  val of_succ_nat : nat -> positive
  end
 
 module N :
@@ -143,20 +156,14 @@ module Z :
 
   val compare : z -> z -> comparison
 
-  val eqb : z -> z -> bool
-
   val leb : z -> z -> bool
 
   val ltb : z -> z -> bool
 
-  val gtb : z -> z -> bool
+  val eqb : z -> z -> bool
 
   val max : z -> z -> z
 
-  val abs : z -> z
-
-  val to_N : z -> n
-
   val of_nat : nat -> z
 
   val of_N : n -> z
@@ -167,7 +174,15 @@ module Z :
 
   val div : z -> z -> z
 
+  val gtb : z -> z -> bool
+
+  val abs : z -> z
+
+  val to_N : z -> n
+
   val gcd : z -> z -> z
+
+  val lcm : z -> z -> z
  end
 
 type 'c pExpr =
@@ -222,7 +237,8 @@ val pmulC_aux : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol ->
 
 val pmulC : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 -> 'a1 pol
 
-val pmulI : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
+val pmulI :
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol -> 'a1 pol) -> 'a1 pol -> positive -> 'a1 pol -> 'a1 pol
 
 val pmul : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
 
@@ -231,12 +247,15 @@ val psquare : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -
 val mk_X : 'a1 -> 'a1 -> positive -> 'a1 pol
 
 val ppow_pos :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol -> positive -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> 'a1 pol ->
+  positive -> 'a1 pol
 
-val ppow_N : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
+val ppow_N :
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 pol -> 'a1 pol) -> 'a1 pol -> n -> 'a1 pol
 
 val norm_aux :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr ->
+  'a1 pol
 
 type kind =
 | IsProp
@@ -308,34 +327,36 @@ val and_cnf_opt : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
 val or_cnf_opt : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf
 
 val mk_and :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4,
-  'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1,
+  'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
 
 val mk_or :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4,
-  'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1,
+  'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
 
 val mk_impl :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4,
-  'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1,
+  'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
 
 val mk_iff :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1, 'a3, 'a4,
-  'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf) -> kind -> bool -> ('a1,
+  'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
 
 val is_bool : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool option
 
 val xcnf :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5)
-  tFormula -> ('a2, 'a3) cnf
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1,
+  'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf
 
 val radd_term : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) -> ('a1, 'a2) clause -> (('a1, 'a2) clause, 'a2 trace) sum
 
 val ror_clause : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause -> (('a1, 'a2) clause, 'a2 trace) sum
 
-val xror_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace
+val xror_clause_cnf :
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace
 
-val ror_clause_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace
+val ror_clause_cnf :
+  ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list * 'a2 trace
 
 val ror_cnf : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) clause list -> ('a1, 'a2) clause list -> ('a1, 'a2) cnf * 'a2 trace
 
@@ -344,82 +365,84 @@ val ror_cnf_opt : ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf
 val ratom : ('a1, 'a2) cnf -> 'a2 -> ('a1, 'a2) cnf * 'a2 trace
 
 val rxcnf_and :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool -> kind -> ('a1,
-  'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool ->
+  kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
 
 val rxcnf_or :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool -> kind -> ('a1,
-  'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool ->
+  kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
 
 val rxcnf_impl :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool -> kind -> ('a1,
-  'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool ->
+  kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
 
 val rxcnf_iff :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool -> kind -> ('a1,
-  'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> (bool -> kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace) -> bool ->
+  kind -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a1, 'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
 
 val rxcnf :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1, 'a3, 'a4, 'a5)
-  tFormula -> ('a2, 'a3) cnf * 'a3 trace
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> bool -> kind -> ('a1,
+  'a3, 'a4, 'a5) tFormula -> ('a2, 'a3) cnf * 'a3 trace
 
 type ('term, 'annot, 'tX) to_constrT = { mkTT : (kind -> 'tX); mkFF : (kind -> 'tX); mkA : (kind -> 'term -> 'annot -> 'tX);
-                                         mkAND : (kind -> 'tX -> 'tX -> 'tX); mkOR : (kind -> 'tX -> 'tX -> 'tX); mkIMPL : (kind -> 'tX -> 'tX -> 'tX);
-                                         mkIFF : (kind -> 'tX -> 'tX -> 'tX); mkNOT : (kind -> 'tX -> 'tX); mkEQ : ('tX -> 'tX -> 'tX) }
+                                         mkAND : (kind -> 'tX -> 'tX -> 'tX); mkOR : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkIMPL : (kind -> 'tX -> 'tX -> 'tX); mkIFF : (kind -> 'tX -> 'tX -> 'tX);
+                                         mkNOT : (kind -> 'tX -> 'tX); mkEQ : ('tX -> 'tX -> 'tX) }
 
 val aformula : ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3
 
 val is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> 'a3 option
 
 val abs_and :
-  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1,
-  'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
+  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4)
+  tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
 
 val abs_or :
-  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1,
-  'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
+  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4)
+  tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
 
 val abs_not :
-  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) ->
-  ('a1, 'a3, 'a2, 'a4) gFormula
+  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> (kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4)
+  tFormula) -> ('a1, 'a3, 'a2, 'a4) gFormula
 
 val mk_arrow : 'a4 option -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val abst_simpl : ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val abst_and :
-  ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4)
-  tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1,
+  'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val abst_or :
-  ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4)
-  tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind -> ('a1,
+  'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val abst_impl :
-  ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> 'a4 option -> kind -> ('a1,
-  'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> 'a4 option ->
+  kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val or_is_X : kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> bool
 
 val abs_iff :
-  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2,
-  'a3, 'a4) tFormula -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula ->
+  ('a1, 'a2, 'a3, 'a4) tFormula -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val abst_iff :
-  ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> kind ->
-  ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool
+  -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val abst_eq :
-  ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool -> ('a1, 'a2,
-  'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
+  ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> (bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula) -> bool
+  -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
-val abst_form : ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
+val abst_form :
+  ('a1, 'a2, 'a3) to_constrT -> ('a2 -> bool) -> bool -> kind -> ('a1, 'a2, 'a3, 'a4) tFormula -> ('a1, 'a2, 'a3, 'a4) tFormula
 
 val cnf_checker : (('a1 * 'a2) list -> 'a3 -> bool) -> ('a1, 'a2) cnf -> 'a3 list -> bool
 
 val tauto_checker :
-  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list -> 'a4 -> bool) ->
-  ('a1, rtyp, 'a3, unit0) gFormula -> 'a4 list -> bool
+  ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> ('a1 -> 'a3 -> ('a2, 'a3) cnf) -> (('a2 * 'a3) list ->
+  'a4 -> bool) -> ('a1, rtyp, 'a3, unit0) gFormula -> 'a4 list -> bool
 
 val cneqb : ('a1 -> 'a1 -> bool) -> 'a1 -> 'a1 -> bool
 
@@ -462,13 +485,14 @@ val nformula_times_nformula :
 val nformula_plus_nformula : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> 'a1 nFormula -> 'a1 nFormula option
 
 val eval_Psatz :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> 'a1
-  nFormula option
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1
+  psatz -> 'a1 nFormula option
 
 val check_inconsistent : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula -> bool
 
 val check_normalised_formulas :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1 psatz -> bool
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a1
+  psatz -> bool
 
 type op2 =
 | OpEq
@@ -480,7 +504,9 @@ type op2 =
 
 type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
 
-val norm : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol
+val norm :
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr ->
+  'a1 pol
 
 val psub0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol
 
@@ -489,7 +515,8 @@ val padd0 : 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1
 val popp0 : ('a1 -> 'a1) -> 'a1 pol -> 'a1 pol
 
 val normalise :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula -> 'a1 nFormula
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 formula ->
+  'a1 nFormula
 
 val xnormalise : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list
 
@@ -498,12 +525,12 @@ val xnegate : ('a1 -> 'a1) -> 'a1 nFormula -> 'a1 nFormula list
 val cnf_of_list : 'a1 -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1 nFormula list -> 'a2 -> ('a1 nFormula, 'a2) cnf
 
 val cnf_normalise :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1
-  formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 ->
+  bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
 
 val cnf_negate :
-  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 -> bool) -> 'a1
-  formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
+  'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> ('a1 -> 'a1 ->
+  bool) -> 'a1 formula -> 'a2 -> ('a1 nFormula, 'a2) cnf
 
 val xdenorm : positive -> 'a1 pol -> 'a1 pExpr
 
@@ -515,42 +542,31 @@ val map_Formula : ('a2 -> 'a1) -> 'a2 formula -> 'a1 formula
 
 val simpl_cone : 'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 psatz -> 'a1 psatz
 
-type q = { qnum : z; qden : positive }
-
-val qeq_bool : q -> q -> bool
-
-val qle_bool : q -> q -> bool
-
-val qplus : q -> q -> q
-
-val qmult : q -> q -> q
-
-val qopp : q -> q
+module PositiveSet :
+ sig
+  type tree =
+  | Leaf
+  | Node of tree * bool * tree
 
-val qminus : q -> q -> q
+  type t = tree
 
-val qinv : q -> q
+  val empty : t
 
-val qpower_positive : q -> positive -> q
+  val mem : positive -> t -> bool
 
-val qpower : q -> z -> q
+  val add : positive -> t -> t
+ end
 
-type 'a t =
+type 'a t0 =
 | Empty
 | Elt of 'a
-| Branch of 'a t * 'a * 'a t
+| Branch of 'a t0 * 'a * 'a t0
 
-val find : 'a1 -> 'a1 t -> positive -> 'a1
+val find : 'a1 -> 'a1 t0 -> positive -> 'a1
 
-val singleton : 'a1 -> positive -> 'a1 -> 'a1 t
+val singleton : 'a1 -> positive -> 'a1 -> 'a1 t0
 
-val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t -> 'a1 t
-
-val zeval_const : z pExpr -> z option
-
-type zWitness = z psatz
-
-val zWeakChecker : z nFormula list -> z psatz -> bool
+val vm_add : 'a1 -> positive -> 'a1 -> 'a1 t0 -> 'a1 t0
 
 val psub1 : z pol -> z pol -> z pol
 
@@ -558,7 +574,7 @@ val popp1 : z pol -> z pol
 
 val padd1 : z pol -> z pol -> z pol
 
-val normZ : z pExpr -> z pol
+val norm0 : z pExpr -> z pol
 
 val zunsat : z nFormula -> bool
 
@@ -566,20 +582,18 @@ val zdeduce : z nFormula -> z nFormula -> z nFormula option
 
 val xnnormalise : z formula -> z nFormula
 
-val xnormalise0 : z nFormula -> z nFormula list
-
-val cnf_of_list0 : 'a1 -> z nFormula list -> (z nFormula * 'a1) list list
+val xis_integral : (positive -> bool) -> positive -> z pol -> bool
 
-val normalise0 : z formula -> 'a1 -> (z nFormula, 'a1) cnf
+val get : PositiveSet.t -> positive -> bool
 
-val xnegate0 : z nFormula -> z nFormula list
+val oget : PositiveSet.t option -> positive -> bool
 
-val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf
-
-val cnfZ : kind -> (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 trace
+val is_integral : PositiveSet.t option -> z pol -> bool
 
 val ceiling : z -> z -> z
 
+type zWitness = z psatz
+
 type zArithProof =
 | DoneProof
 | RatProof of zWitness * zArithProof
@@ -614,10 +628,50 @@ val max_var : positive -> z pol -> positive
 
 val max_var_nformulae : z nFormula list -> positive
 
-val zChecker : z nFormula list -> zArithProof -> bool
+val add0 : positive -> PositiveSet.t option -> PositiveSet.t option
+
+val zChecker : PositiveSet.t option -> z nFormula list -> zArithProof -> bool
+
+val zeval_const : z pExpr -> z option
+
+val zWeakChecker : z nFormula list -> z psatz -> bool
+
+val normZ : z pExpr -> z pol
+
+val cnf_of_list0 : 'a1 -> z nFormula list -> (z nFormula * 'a1) list list
+
+val xnormalise0 : z nFormula -> z nFormula list
+
+val normalise0 : z formula -> 'a1 -> (z nFormula, 'a1) cnf
+
+val xnegate0 : z nFormula -> z nFormula list
+
+val negate : z formula -> 'a1 -> (z nFormula, 'a1) cnf
+
+val cnfZ : kind -> (z formula, 'a1, 'a2, 'a3) tFormula -> (z nFormula, 'a1) cnf * 'a1 trace
 
 val zTautoChecker : z formula bFormula -> zArithProof list -> bool
 
+type q = { qnum : z; qden : positive }
+
+val qeq_bool : q -> q -> bool
+
+val qle_bool : q -> q -> bool
+
+val qplus : q -> q -> q
+
+val qmult : q -> q -> q
+
+val qopp : q -> q
+
+val qminus : q -> q -> q
+
+val qinv : q -> q
+
+val qpower_positive : q -> positive -> q
+
+val qpower : q -> z -> q
+
 type qWitness = q psatz
 
 val qWeakChecker : q nFormula list -> q psatz -> bool
@@ -652,9 +706,7 @@ val z_of_exp : (z, nat) sum -> z
 
 val q_of_Rcst : rcst -> q
 
-type rWitness = q psatz
-
-val rWeakChecker : q nFormula list -> q psatz -> bool
+type rWitness = zArithProof
 
 val rnormalise : q formula -> 'a1 -> (q nFormula, 'a1) cnf
 
@@ -664,4 +716,32 @@ val runsat : q nFormula -> bool
 
 val rdeduce : q nFormula -> q nFormula -> q nFormula option
 
-val rTautoChecker : rcst formula bFormula -> rWitness list -> bool
+type 'form eFormula =
+| IsZ of bool * positive
+| IsF of 'form
+
+val map_eFormula : ('a1 -> 'a2) -> 'a1 formula eFormula -> 'a2 formula eFormula
+
+val lcm0 : q pol -> z
+
+val polZ : z -> q pol -> z pol
+
+val nformulaZ : q nFormula -> z nFormula
+
+val xcollect_isZ : PositiveSet.t -> z nFormula list -> (q nFormula eFormula * unit0) list -> PositiveSet.t * z nFormula list
+
+val qCheck : (q nFormula eFormula * unit0) list -> zArithProof -> bool
+
+val erunsat : q nFormula eFormula -> bool
+
+val erdeduce : q nFormula eFormula -> q nFormula eFormula -> q nFormula eFormula option
+
+val map_cnf : ('a2 -> 'a3) -> ('a2, 'a1) cnf -> ('a3, 'a1) cnf
+
+val eRnormalise : q formula eFormula -> 'a1 -> (q nFormula eFormula, 'a1) cnf
+
+val eRnegate : q formula eFormula -> 'a1 -> (q nFormula eFormula, 'a1) cnf
+
+val cnfR : kind -> (q formula eFormula, 'a1, 'a2, 'a3) tFormula -> (q nFormula eFormula, 'a1) cnf * 'a1 trace
+
+val rTautoChecker : rcst formula eFormula bFormula -> rWitness list -> bool
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index dbdac50cc9c0..81d25e90badb 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.ml
@@ -36,6 +36,14 @@ module IMap = struct
     r
 end
 
+let pp_smt_num o q =
+  let nn = Q.num q in
+  let dn = Q.den q in
+  if Z.equal dn Z.one then output_string o (Z.to_string nn)
+  else Printf.fprintf o "(/ %s %s)" (Z.to_string nn) (Z.to_string dn)
+
+
+
 let rec pp_list s f o l =
   match l with
   | [] -> ()
@@ -424,6 +432,7 @@ module Hash = struct
       eq_pol eq p1 p2 && eq_positive i1 i2 && eq_pol eq p1' p2'
     | _, _ -> false
 
+
   let eq_pair eq1 eq2 (x1, y1) (x2, y2) = eq1 x1 x2 && eq2 y1 y2
 
   let hash_pol helt =
diff --git a/plugins/micromega/mutils.mli b/plugins/micromega/mutils.mli
index 2f7c980c8a0a..06b741edf86a 100644
--- a/plugins/micromega/mutils.mli
+++ b/plugins/micromega/mutils.mli
@@ -99,6 +99,7 @@ module Hash : sig
   val hash_elt : ('a -> int) -> int -> 'a -> int
 end
 
+val pp_smt_num : out_channel -> Q.t -> unit
 val all_pairs : ('a -> 'a -> 'b) -> 'a list -> 'b list
 val is_sublist : ('a -> 'b -> bool) -> 'a list -> 'b list -> bool
 val extract : ('a -> 'b option) -> 'a list -> ('b * 'a) option * 'a list
diff --git a/plugins/micromega/numCompat.ml b/plugins/micromega/numCompat.ml
index 1728850c3316..7aa25f2ddd84 100644
--- a/plugins/micromega/numCompat.ml
+++ b/plugins/micromega/numCompat.ml
@@ -101,6 +101,7 @@ module type QArith = sig
   val to_string : t -> string
   val of_string : string -> t
   val to_float : t -> float
+  val of_float : float -> t
 end
 
 module Q : QArith with module Z = Z = struct
diff --git a/plugins/micromega/numCompat.mli b/plugins/micromega/numCompat.mli
index 8ce0f3120f74..9ab0742e8366 100644
--- a/plugins/micromega/numCompat.mli
+++ b/plugins/micromega/numCompat.mli
@@ -88,6 +88,7 @@ module type QArith = sig
   val to_string : t -> string
   val of_string : string -> t
   val to_float : t -> float
+  val of_float : float -> t
 end
 
 module Z : ZArith
diff --git a/plugins/micromega/polynomial.ml b/plugins/micromega/polynomial.ml
index 1a61e3468ec1..e3f13f35e645 100644
--- a/plugins/micromega/polynomial.ml
+++ b/plugins/micromega/polynomial.ml
@@ -45,6 +45,7 @@ module Monomial : sig
   val degree : t -> int
   val subset : t -> t -> bool
   val output : out_channel -> t -> unit
+  val is_integer : ISet.t -> t -> bool
 end =
 struct
   type t = int array
@@ -223,6 +224,10 @@ struct
     in
     pp_list o (List.rev @@ fold (fun x v accu -> (x, v) :: accu) m [])
 
+
+  let is_integer s m =
+        fold (fun x _ acc -> ISet.mem x s && acc ) m true
+
 end
 
 module MonMap = struct
@@ -369,7 +374,8 @@ module LinPoly = struct
     (** A hash table might be preferable but requires a hash function. *)
     let (index_of_monomial : int MonoMap.t ref) = ref MonoMap.empty
 
-    let (monomial_of_index : Monomial.t IntMap.t ref) = ref IntMap.empty
+    let (monomial_of_index : Monomial.t  IntMap.t ref) = ref IntMap.empty
+
     let fresh = ref 0
 
     let reserve vr =
@@ -402,6 +408,21 @@ module LinPoly = struct
     let _ = register Monomial.const
   end
 
+  let is_integer isZ v =
+    let module EXIT = struct exception Exit end in
+    match isZ with
+    | None -> true
+    | Some s ->
+       if Vect.is_constant v
+       then false
+       else
+         try
+           Vect.fold (fun acc vr _ ->
+               if not (Monomial.is_integer s (MonT.retrieve vr)) then raise EXIT.Exit) () v;
+           true
+         with EXIT.Exit -> false
+
+
   let var v = Vect.set (MonT.register (Monomial.var v)) Q.one Vect.null
 
   let of_monomial m =
@@ -678,8 +699,87 @@ module ProofFormat = struct
     | ExProof (i, j, k, _, _, _, prf) ->
       max (max (max i j) k) (proof_max_def prf)
 
+  let add_proof x y =
+    match (x, y) with Zero, p | p, Zero -> p | _ -> AddPrf (x, y)
+
+  let rec mul_cst_proof c p =
+    match p with
+    | Annot (s, p) -> Annot (s, mul_cst_proof c p)
+    | MulC (v, p') -> MulC (Vect.mul c v, p')
+    | _ -> (
+      match Q.sign c with
+      | 0 -> Zero (* This is likely to be a bug *)
+      | -1 ->
+        MulC (LinPoly.constant c, p) (* [p] should represent an equality *)
+      | 1 -> if Q.one =/ c then p else MulPrf (Cst c, p)
+      | _ -> assert false )
+
+  let sMulC v p =
+    let c, v' = Vect.decomp_cst v in
+    if Vect.is_null v' then mul_cst_proof c p else MulC (v, p)
+
+  let mul_proof p1 p2 =
+    match (p1, p2) with
+    | Zero, _ | _, Zero -> Zero
+    | Cst c, p | p, Cst c -> mul_cst_proof c p
+    | _, _ -> MulPrf (p1, p2)
+
+
+
+  let rec pr_rule_scale_gcd m lenv p =
+    match p with
+    | Annot(_,p) -> (p,Z.one)
+    | MulC(p,prf) -> let prf', g = pr_rule_scale_gcd m lenv prf in
+                     (MulC(p,prf'),g)
+    | Gcd(z,prf)  -> let prf', g = pr_rule_scale_gcd m lenv prf in
+                     assert (Z.compare z Z.zero = 1);
+                     (prf',Z.mul z g)
+    | MulPrf(prf1,prf2) ->
+       let prf1, g1 = pr_rule_scale_gcd m lenv prf1 in
+       let prf2, g2 = pr_rule_scale_gcd m lenv prf2 in
+       (MulPrf(prf1,prf2),Z.mul g1 g2)
+    | AddPrf(prf1,prf2) ->
+       let prf1, g1 = pr_rule_scale_gcd m lenv prf1 in
+       let prf2, g2 = pr_rule_scale_gcd m lenv prf2 in
+       let lcm = Z.ppcm g1 g2 in
+       let q1  = Q.of_bigint (Z.div lcm g1) in
+       let q2  = Q.of_bigint (Z.div lcm g2) in
+       AddPrf(mul_cst_proof q1 prf1,mul_cst_proof  q2 prf2),lcm
+    | CutPrf p ->
+       let prf1,g = pr_rule_scale_gcd m lenv p in
+       CutPrf prf1, Z.one
+    | LetPrf(p1,p2) ->
+       let prf1,g = pr_rule_scale_gcd m lenv p1 in
+       let prf2,g2 = pr_rule_scale_gcd m (g::lenv) p2 in
+       LetPrf(prf1,prf2), g2
+      | Def i  -> (Def i, try IMap.find i m with Not_found -> Z.one)
+      | Ref i  -> (Ref i,List.nth lenv i)
+      | _      -> (p,Z.one)
+
+  let proof_scale_gcd prf =
+    let rec proof_scale_gcd m prf =
+      match prf with
+      | Done -> Done
+      | Step(i,r,prf) -> let (p',z) = pr_rule_scale_gcd m [] r in
+                         if Z.equal z Z.one
+                         then Step(i,p',proof_scale_gcd m prf)
+                         else Step(i,p',proof_scale_gcd (IMap.add i z m) prf)
+      | Split(i,v,p1,p2) ->
+         Split(i,v,proof_scale_gcd m p1, proof_scale_gcd m p2)
+      | Enum(i,r1,v1,r2,l) ->
+         let r1,_ = pr_rule_scale_gcd m [] r1 in
+         let r2,_ = pr_rule_scale_gcd m [] r2 in
+         Enum(i,r1,v1,r2,List.map (proof_scale_gcd m) l)
+      | ExProof(x,y,z,v1,v2,v3,prf) ->
+         ExProof(z,y,z,v1,v2,v3,proof_scale_gcd m prf)
+    in proof_scale_gcd IMap.empty prf
+
+
+
+
+
   (** [pr_rule_def_cut id pr] gives an explicit [id] to cut rules.
-      This is because the Rocq proof format only accept they as a proof-step *)
+      This is because the Rocq proof format only accept them as a proof-step *)
   let pr_rule_def_cut m id p =
     let rec pr_rule_def_cut m id = function
       | Annot (_, p) -> pr_rule_def_cut m id p
@@ -698,7 +798,8 @@ module ProofFormat = struct
         let bds1, m, id, p1 = pr_rule_def_cut m id p1 in
         let bds2, m, id, p2 = pr_rule_def_cut m id p2 in
         (bds2 @ bds1, m, id, LetPrf (p1, p2))
-      | CutPrf p | Gcd (_, p) -> (
+      | Gcd (_, p) -> assert false (* removed by pr_rule_scale_gcd *)
+      | CutPrf p  -> (
         let bds, m, id, p = pr_rule_def_cut m id p in
         try
           let id' = PrfRuleMap.find p m in
@@ -731,30 +832,6 @@ module ProofFormat = struct
       ISet.union (pr_rule_collect_defs p1) (pr_rule_collect_defs p2)
 
 
-  let add_proof x y =
-    match (x, y) with Zero, p | p, Zero -> p | _ -> AddPrf (x, y)
-
-  let rec mul_cst_proof c p =
-    match p with
-    | Annot (s, p) -> Annot (s, mul_cst_proof c p)
-    | MulC (v, p') -> MulC (Vect.mul c v, p')
-    | _ -> (
-      match Q.sign c with
-      | 0 -> Zero (* This is likely to be a bug *)
-      | -1 ->
-        MulC (LinPoly.constant c, p) (* [p] should represent an equality *)
-      | 1 -> if Q.one =/ c then p else MulPrf (Cst c, p)
-      | _ -> assert false )
-
-  let sMulC v p =
-    let c, v' = Vect.decomp_cst v in
-    if Vect.is_null v' then mul_cst_proof c p else MulC (v, p)
-
-  let mul_proof p1 p2 =
-    match (p1, p2) with
-    | Zero, _ | _, Zero -> Zero
-    | Cst c, p | p, Cst c -> mul_cst_proof c p
-    | _, _ -> MulPrf (p1, p2)
 
   let prf_rule_of_map m =
     PrfRuleMap.fold (fun k v acc -> add_proof (sMulC v k) acc) m Zero
@@ -886,28 +963,6 @@ module ProofFormat = struct
         (snd res);
     res
 
-  (*
-  let mul_proof p1 p2 =
-    let res = mul_proof p1 p2 in
-    Printf.printf "mul_proof %a %a = %a\n"
-    output_prf_rule p1 output_prf_rule p2 output_prf_rule res; res
-
-  let add_proof p1 p2 =
-    let res = add_proof p1 p2 in
-    Printf.printf "add_proof %a %a = %a\n"
-    output_prf_rule p1 output_prf_rule p2 output_prf_rule res; res
-
-
-  let sMulC v p =
-    let res = sMulC v p in
-    Printf.printf "sMulC %a %a = %a\n" Vect.pp v output_prf_rule p output_prf_rule res ;
-    res
-
-  let mul_cst_proof c p  =
-    let res = mul_cst_proof c p in
-    Printf.printf "mul_cst_proof %s %a = %a\n" (Num.string_of_num c) output_prf_rule p output_prf_rule res ;
-    res
- *)
 
   let proof_of_farkas env vect =
     Vect.fold
@@ -1010,6 +1065,7 @@ module ProofFormat = struct
         (CamlToCoq.positive x, cmpl_proof (Env.push_def i  (Env.push_def j (Env.push_def k env))) prf)
 
   let compile_proof env prf =
+    let prf = proof_scale_gcd prf in
     let id = 1 + proof_max_def prf in
     let _, prf = normalise_proof id prf in
     cmpl_proof env prf
@@ -1025,6 +1081,8 @@ module WithProof = struct
 
   let polynomial ((p, _), _) = p
 
+  let is_integer isZ ((p,_),_) = LinPoly.is_integer isZ p
+
   (* The comparison ignores proofs on purpose *)
   let compare : t -> t -> int =
    fun ((lp1, o1), _) ((lp2, o2), _) ->
@@ -1089,25 +1147,40 @@ module WithProof = struct
   let square p q = ((p, Ge), ProofFormat.Square q)
 
   let cutting_plane ((p, o), prf) =
+    (* All the coefficients need to be integers! *)
     let c, p' = Vect.decomp_cst p in
+    let c = if o = Gt then c -/ Q.one else c in
     let g = Vect.gcd p' in
-    if Z.equal Z.one g || c =/ Q.zero || not (Z.equal (Q.den c) Z.one) then None
-      (* Nothing to do *)
+    if Z.equal Z.one g
+    then if o = Gt
+         then Some ((Vect.set 0 c p,Ge),ProofFormat.CutPrf prf)
+         else None
     else
       let c1 = c // Q.of_bigint g in
       let c1' = Q.floor c1 in
-      if c1 =/ c1' then None
+      if c1 =/ c1' && o <> Gt then None
       else
         match o with
         | Eq ->
           Some ((Vect.set 0 Q.minus_one Vect.null, Eq), ProofFormat.CutPrf prf)
-        | Gt -> failwith "cutting_plane ignore strict constraints"
+        (* This is a non-trivial common divisor *)
+        | Gt -> Some
+                  ( (Vect.set 0 c1' (Vect.div (Q.of_bigint g) p), Ge)
+                  , ProofFormat.CutPrf prf )
         | Ge ->
-          (* This is a non-trivial common divisor *)
           Some
             ( (Vect.set 0 c1' (Vect.div (Q.of_bigint g) p), o)
             , ProofFormat.CutPrf prf )
 
+  let cutting_plane_isz isz wp =
+    if is_integer isz wp
+    then
+      begin
+      cutting_plane wp
+      end
+    else None
+
+
   let construct_sign p =
     let c, p' = Vect.decomp_cst p in
     if Vect.is_null p' then
@@ -1181,7 +1254,7 @@ module WithProof = struct
         | _ -> None )
       | (Ge | Gt), Eq -> failwith "pivot: equality as second argument"
 
-  let linear_pivot sys ((lp1, op1), prf1) x ((lp2, op2), prf2) =
+  let linear_pivot (sys: t list) (((lp1, op1), prf1):t) x (((lp2, op2), prf2):t) : t option =
     match linear_pivot sys ((lp1, op1), prf1) x ((lp2, op2), prf2) with
     | None -> None
     | Some (c, p) -> Some (c, ProofFormat.simplify_prf_rule p)
@@ -1206,6 +1279,7 @@ module WithProof = struct
     in
     List.sort cmp (List.rev_map (fun wp -> (size wp, wp)) sys)
 
+
   let iterate_pivot p sys0 =
     let elim sys =
       let oeq, sys' = extract p sys in
@@ -1213,6 +1287,7 @@ module WithProof = struct
       | None -> None
       | Some (v, pc) -> simplify (linear_pivot sys0 pc v) sys'
     in
+
     iterate_until_stable elim (List.map snd (sort sys0))
 
   let subst_constant is_int sys =
@@ -1231,6 +1306,40 @@ module WithProof = struct
     in
     iterate_pivot is_constant sys
 
+  let subst_simple strict sys =
+
+    let get_variable x1 x2 =
+      match Monomial.get_var (LinPoly.MonT.retrieve x1) , Monomial.get_var (LinPoly.MonT.retrieve x2) with
+          | Some x1 , Some x2 -> Some (x1,x2)
+          | _ , _ -> None
+    in
+
+    let is_simple_subst p =
+      match Vect.Classify.classify p with
+      | None -> None
+      | Some (Vect.Classify.IsCst(c,a,x)) ->
+         if not (strict) || Q.abs a = Q.one
+         then Monomial.get_var (LinPoly.MonT.retrieve x)
+         else None
+      | Some (Vect.Classify.IsVar(a1,x1,a2,x2)) ->
+         match get_variable x1 x2 with
+         | None -> None
+         | Some (x1,x2) ->
+            if not strict
+            then (* Give priority to smallest coefficient *)
+              if a1 </ a2 then Some x1 else Some x2
+            else
+              if Q.abs a1 = Q.one then Some x1
+              else if Q.abs a2 = Q.one then Some x2
+              else None in
+
+    let is_simple ((p,o),prf) =
+      if o = Eq then is_simple_subst p
+      else None
+    in
+
+    iterate_pivot is_simple sys
+
   let subst sys0 = iterate_pivot (is_substitution true) sys0
 
   let saturate_subst b sys0 =
diff --git a/plugins/micromega/polynomial.mli b/plugins/micromega/polynomial.mli
index 5d62c910a8d9..c912eca8993b 100644
--- a/plugins/micromega/polynomial.mli
+++ b/plugins/micromega/polynomial.mli
@@ -172,6 +172,11 @@ module LinPoly : sig
       i.e can be written c*x+r where c is a constant and r is independent from x *)
   val is_linear_for : var -> t -> bool
 
+  (** [is_integer isZ v]
+      @return true if the polynomila is built
+        from integer variables *)
+  val is_integer : ISet.t option -> t -> bool
+
   (** [constant c]
       @return the constant polynomial c
    *)
@@ -280,6 +285,8 @@ module WithProof : sig
 
   val polynomial : t -> LinPoly.t
 
+  val is_integer : ISet.t option -> t -> bool
+
   val compare : t -> t -> int
   val annot : string -> t -> t
   val of_cstr : cstr * ProofFormat.prf_rule -> t
@@ -325,6 +332,9 @@ module WithProof : sig
   (** [cutting_plane p] does integer reasoning and adjust the constant to be integral *)
   val cutting_plane : t -> t option
 
+  (** [cutting_plane_isz p] does integer reasoning and adjust the constant to be integral *)
+  val cutting_plane_isz : ISet.t option -> t -> t option
+
   (** [linear_pivot sys p x q]
       @return the polynomial [q] where [x] is eliminated using the polynomial [p]
       The pivoting operation is only defined if
@@ -355,6 +365,12 @@ module WithProof : sig
       only if there is an equation a.x = c for a,c a constant and a divides c if b= true*)
   val subst_constant : bool -> t list -> t list
 
+ (** [subst_simple b sys] performs the equivalent of the `subst` tactic of Rocq
+     only if there is an equation of the form a.x = c or a.x = b.y.
+     If b = true, we require a or b to be 1 or -1
+  *)
+  val subst_simple : bool -> t list -> t list
+
   val saturate_subst : bool -> t list -> t list
 end
 
diff --git a/plugins/micromega/simplex.ml b/plugins/micromega/simplex.ml
index fa7597530ce2..5a418b7b7a2c 100644
--- a/plugins/micromega/simplex.ml
+++ b/plugins/micromega/simplex.ml
@@ -135,7 +135,9 @@ type iset = unit IMap.t
 
 (** Mapping basic variables to their equation.
                                  All variables >= than a threshold rst are restricted.*)
-type tableau = Vect.t IMap.t
+type tableau = InfVect.t IMap.t
+type solution = Inf.t IMap.t
+type qsolution = Vect.t
 
 module Restricted = struct
   type t =
@@ -165,9 +167,11 @@ module Restricted = struct
       (IMap.from rst.base m) acc
 end
 
-let pp_row o v = LinPoly.pp o v
+let pp_row o v =
+  let (i,v) = InfVect.decomp_cst v in
+  Printf.fprintf o "%a + %a"  Inf.pp i LinPoly.pp  v
 
-let output_tableau o t =
+let output_tableau o (t:tableau) =
   IMap.iter
     (fun k v -> Printf.fprintf o "%a = %a\n" LinPoly.pp_var k pp_row v)
     t
@@ -186,9 +190,9 @@ let output_vars o m =
    if ci>=0.
  *)
 
-let unfeasible (rst : Restricted.t) tbl =
+let unfeasible (rst : Restricted.t) (tbl:tableau) =
   Restricted.fold rst
-    (fun k v m -> if Vect.get_cst v >=/ Q.zero then m else IMap.add k () m)
+    (fun k v m -> if Inf.ge_0 (InfVect.get_cst v)  then m else IMap.add k () m)
     tbl IMap.empty
 
 let is_feasible rst tb = IMap.is_empty (unfeasible rst tb)
@@ -217,7 +221,7 @@ let is_maximised_vect rst v =
  *)
 let is_maximised rst v =
   try
-    let vl, v = Vect.decomp_cst v in
+    let vl, v = InfVect.decomp_cst v in
     if is_maximised_vect rst v then Some vl else None
   with Not_found -> None
 
@@ -231,11 +235,11 @@ let is_maximised rst v =
  *)
 
 type result =
-  | Max of Q.t  (** Maximum is reached *)
+  | Max of Inf.t   (** Maximum is reached *)
   | Ubnd of var  (** Problem is unbounded *)
   | Feas  (** Problem is feasible *)
 
-type pivot = Done of result | Pivot of int * int * Q.t
+type pivot = Done of result | Pivot of int * int * Inf.t
 type simplex = Opt of tableau * result
 
 (** For a row, x = ao.xo+...+ai.xi
@@ -268,23 +272,23 @@ let min_score s (i1, sc1) =
   match s with
   | None -> Some (i1, sc1)
   | Some (i0, sc0) ->
-    if sc0 </ sc1 then s
-    else if sc1 </ sc0 then Some (i1, sc1)
+    if Inf.lt sc0  sc1 then s
+    else if Inf.lt sc1  sc0 then Some (i1, sc1)
     else if i0 < i1 then s
     else Some (i1, sc1)
 
-let find_pivot_row rst tbl j sgn =
+let find_pivot_row rst (tbl:tableau) j sgn =
   Restricted.fold rst
     (fun i' v res ->
-      let aij = Vect.get j v in
+      let aij = InfVect.get j v in
       if Q.of_int sgn */ aij </ Q.zero then
         (* This would improve *)
-        let score' = Q.abs (Vect.get_cst v // aij) in
+        let score' = Inf.abs (Inf.divc (InfVect.get_cst v)  aij) in
         min_score res (i', score')
       else res)
     tbl None
 
-let safe_find err x t =
+let safe_find err x (t:tableau) =
   try IMap.find x t
   with Not_found ->
     if debug then
@@ -299,7 +303,7 @@ let find_pivot vr (rst : Restricted.t) tbl =
   | Some mx -> Done (Max mx) (* Maximum is reached; we are done *)
   | None -> (
     (* Extract the vector *)
-    let _, v = Vect.decomp_cst v in
+    let _, v = InfVect.decomp_cst v in
     let j', sgn = find_pivot_column rst v in
     match find_pivot_row rst (IMap.remove vr tbl) j' sgn with
     | None -> Done (Ubnd j')
@@ -314,24 +318,24 @@ let find_pivot vr (rst : Restricted.t) tbl =
      c = (r - e')/ai
  *)
 
-let solve_column (c : var) (r : var) (e : Vect.t) : Vect.t =
-  let a = Vect.get c e in
+let solve_column (c : var) (r : var) (e : InfVect.t) : InfVect.t =
+  let a = InfVect.get c e in
   if a =/ Q.zero then failwith "Cannot solve column"
   else
     let a' = Q.minus_one // a in
-    Vect.mul a' (Vect.set r Q.minus_one (Vect.set c Q.zero e))
+    InfVect.mul a' (InfVect.set r Q.minus_one (InfVect.set c Q.zero e))
 
 (** [pivot_row r c e]
     @param c is such that c = e
     @param r is a vector r = g.c + r'
     @return g.e+r' *)
 
-let pivot_row (row : Vect.t) (c : var) (e : Vect.t) : Vect.t =
-  let g = Vect.get c row in
-  if g =/ Q.zero then row else Vect.mul_add g e Q.one (Vect.set c Q.zero row)
+let pivot_row (row : InfVect.t) (c : var) (e : InfVect.t) : InfVect.t =
+  let g = InfVect.get c row in
+  if g =/ Q.zero then row else InfVect.mul_add g e Q.one (InfVect.set c Q.zero row)
 
-let pivot_with (m : tableau) (v : var) (p : Vect.t) =
-  IMap.map (fun (r : Vect.t) -> pivot_row r v p) m
+let pivot_with (m : tableau) (v : var) (p : InfVect.t) =
+  IMap.map (fun (r : InfVect.t) -> pivot_row r v p) m
 
 let pivot (m : tableau) (r : var) (c : var) =
   incr nb_pivot;
@@ -339,8 +343,8 @@ let pivot (m : tableau) (r : var) (c : var) =
   let piv = solve_column c r row in
   IMap.add c piv (pivot_with (IMap.remove r m) c piv)
 
-let adapt_unbounded vr x rst tbl =
-  if Vect.get_cst (IMap.find vr tbl) >=/ Q.zero then tbl else pivot tbl vr x
+let adapt_unbounded vr x rst (tbl:tableau) =
+  if  Inf.ge_0 (InfVect.get_cst (IMap.find vr tbl)) then tbl else pivot tbl vr x
 
 module BaseSet = Set.Make (struct
   type t = iset
@@ -350,9 +354,9 @@ end)
 
 let get_base tbl = IMap.mapi (fun k _ -> ()) tbl
 
-let simplex opt vr rst tbl =
+let simplex opt vr rst (tbl:tableau) =
   let b = ref BaseSet.empty in
-  let rec simplex opt vr rst tbl =
+  let rec simplex opt vr rst (tbl:tableau) =
     ( if debug then
       let base = get_base tbl in
       if BaseSet.mem base !b then Printf.fprintf stdout "Cycling detected\n"
@@ -365,7 +369,7 @@ let simplex opt vr rst tbl =
       output_tableau stdout tbl;
       Printf.fprintf stdout "Error for variables %a\n" output_vars m
     end;
-    if (not opt) && Vect.get_cst (IMap.find vr tbl) >=/ Q.zero then
+    if (not opt) && Inf.ge_0 (InfVect.get_cst (IMap.find vr tbl)) then
       Opt (tbl, Feas)
     else
       match find_pivot vr rst tbl with
@@ -378,7 +382,7 @@ let simplex opt vr rst tbl =
         | Feas -> raise (Invalid_argument "find_pivot") )
       | Pivot (i, j, s) ->
         if debug then begin
-          Printf.fprintf stdout "Find pivot for x%i(%s)\n" vr (Q.to_string s);
+          Printf.fprintf stdout "Find pivot for x%i(%a)\n" vr Inf.pp s;
           Printf.fprintf stdout "Leaving variable x%i\n" i;
           Printf.fprintf stdout "Entering variable x%i\n" j
         end;
@@ -393,29 +397,31 @@ type certificate = Unsat of Vect.t | Sat of tableau * var option
     @return a row obtained by pivoting the basic variables of the vector v
  *)
 
-let normalise_row (t : tableau) (v : Vect.t) =
+let normalise_row (t : tableau) (v : InfVect.t) =
+  let (i,v) = InfVect.decomp_cst v in
   Vect.fold
     (fun acc vr ai ->
       try
         let e = IMap.find vr t in
-        Vect.add (Vect.mul ai e) acc
-      with Not_found -> Vect.add (Vect.set vr ai Vect.null) acc)
-    Vect.null v
+        InfVect.add (InfVect.mul ai e) acc
+      with Not_found -> InfVect.add (InfVect.set vr ai InfVect.null) acc)
+    (InfVect.of_cst i) v
 
-let normalise_row (t : tableau) (v : Vect.t) =
+
+let normalise_row (t : tableau) (v : InfVect.t) =
   let v' = normalise_row t v in
-  if debug then Printf.fprintf stdout "Normalised Optimising %a\n" LinPoly.pp v';
+  if debug then Printf.fprintf stdout "Normalised Optimising %a\n" pp_row v';
   v'
 
-let add_row (nw : var) (t : tableau) (v : Vect.t) : tableau =
+let add_row (nw : var) (t : tableau) (v : InfVect.t) : tableau =
   IMap.add nw (normalise_row t v) t
 
 (** [push_real] performs reasoning over the rationals *)
-let push_real (opt : bool) (nw : var) (v : Vect.t) (rst : Restricted.t)
+let push_real (opt : bool) (nw : var) (v : InfVect.t) (rst : Restricted.t)
     (t : tableau) : certificate =
   if debug then begin
     Printf.fprintf stdout "Current Tableau\n%a\n" output_tableau t;
-    Printf.fprintf stdout "Optimising %a=%a\n" LinPoly.pp_var nw LinPoly.pp v
+    Printf.fprintf stdout "Optimising %a=%a\n" LinPoly.pp_var nw pp_row v
   end;
   match simplex opt nw rst (add_row nw t v) with
   | Opt (t', r) -> (
@@ -429,12 +435,13 @@ let push_real (opt : bool) (nw : var) (v : Vect.t) (rst : Restricted.t)
     | Feas -> Sat (t', None)
     | Max n ->
       if debug then begin
-        Printf.printf "The objective is maximised %s\n" (Q.to_string n);
+        Printf.printf "The objective is maximised %a\n" Inf.pp n;
         Printf.printf "%a = %a\n" LinPoly.pp_var nw pp_row (IMap.find nw t')
       end;
-      if n >=/ Q.zero then Sat (t', None)
+      if Inf.ge_0 n then Sat (t', None)
       else
         let v' = safe_find "push_real" nw t' in
+        let v' = snd (InfVect.decomp_cst v') in
         Unsat (Vect.set nw Q.one (Vect.set 0 Q.zero (Vect.mul Q.minus_one v')))
     )
 
@@ -446,33 +453,46 @@ open Polynomial
 
 (*type varmap = (int * bool) IMap.t*)
 
-let find_solution rst tbl =
-  IMap.fold
-    (fun vr v res ->
-      if Restricted.is_restricted vr rst then res
-      else Vect.set vr (Vect.get_cst v) res)
-    tbl Vect.null
+let find_solution rst (tbl:tableau) : solution =
+  IMap.filter_map
+              (fun vr v ->
+                if Restricted.is_restricted vr rst then None
+                else Some (InfVect.get_cst v))
+              tbl
+
+(* let find_full_solution rst (tbl:tableau) =
+   IMap.map (fun  v -> InfVect.get_cst v) tbl *)
+
+let find_q_solution rst (tbl:tableau) =
+  IMap.fold (fun vr v res ->
+      let c = fst (Inf.decomp (InfVect.get_cst v)) in
+      Vect.set vr c res) tbl Vect.null
 
-let find_full_solution rst tbl =
-  IMap.fold (fun vr v res -> Vect.set vr (Vect.get_cst v) res) tbl Vect.null
 
-let choose_conflict (sol : Vect.t) (l : (var * Vect.t) list) =
-  let esol = Vect.set 0 Q.one sol in
+
+let eval_solution sol v =
+  let (c,v) = InfVect.decomp_cst v in
+  Vect.fold (fun acc k c ->
+      try
+        Inf.add acc (Inf.mulc c (IMap.find k sol))
+      with  Not_found -> acc) c v
+
+let choose_conflict (sol : solution) (l : (var * InfVect.t) list) =
   let rec most_violating l e (x, v) rst =
     match l with
     | [] -> Some ((x, v), rst)
     | (x', v') :: l ->
-      let e' = Vect.dotproduct esol v' in
-      if e' <=/ e then most_violating l e' (x', v') ((x, v) :: rst)
+      let e' = eval_solution sol v' in
+      if Inf.lt e' e then most_violating l e' (x', v') ((x, v) :: rst)
       else most_violating l e (x, v) ((x', v') :: rst)
   in
   match l with
   | [] -> None
   | (x, v) :: l ->
-    let e = Vect.dotproduct esol v in
+    let e = eval_solution sol v in
     most_violating l e (x, v) []
 
-let rec solve opt l (rst : Restricted.t) (t : tableau) =
+let rec solve opt (l:(var * InfVect.t) list) (rst : Restricted.t) (t : tableau) =
   let sol = find_solution rst t in
   match choose_conflict sol l with
   | None -> Inl (rst, t, None)
@@ -514,18 +534,20 @@ module PrfEnv = struct
     | wp :: l -> (
       let ((lp, op), prf) = WithProof.repr wp in
       match op with
-      | Gt -> raise Strict (* Should be eliminated earlier *)
+      | Gt ->
+         let f, env' = register wp env in
+         of_list ((f, InfVect.of_vect lp true) :: acc) env' l
       | Ge ->
         (* Simply register *)
         let f, env' = register wp env in
-        of_list ((f, lp) :: acc) env' l
+        of_list ((f, InfVect.of_vect lp false) :: acc) env' l
       | Eq ->
         (* Generate two constraints *)
         let f1, env = register wp env in
         let wp' = WithProof.neg wp in
         let f2, env = register wp' env in
         let (lp', _), _ = WithProof.repr wp' in
-        of_list ((f1, lp) :: (f2, lp') :: acc) env l )
+        of_list ((f1, InfVect.of_vect lp false) :: (f2, InfVect.of_vect lp' false) :: acc) env l )
 
   let map f env = IMap.map f env
 end
@@ -535,14 +557,6 @@ let make_env (l : Polynomial.cstr list) =
     (List.rev_map WithProof.of_cstr
        (List.mapi (fun i x -> (x, ProofFormat.Hyp i)) l))
 
-let find_point (l : Polynomial.cstr list) =
-  let vr = fresh_var l in
-  LinPoly.MonT.safe_reserve vr;
-  let l', _ = make_env l in
-  match solve false l' (Restricted.make vr) IMap.empty with
-  | Inl (rst, t, _) -> Some (find_solution rst t)
-  | _ -> None
-
 (** [make_certificate env l] makes very strong assumptions
     about the form of the environment.
     Each proof is assumed to be either:
@@ -600,8 +614,9 @@ let violation sol vect =
   if Q.zero =/ c then Vect.dotproduct sol vect
   else Q.abs (Vect.dotproduct sol vect // c)
 
-let cut env rmin sol (rst : Restricted.t) tbl (x, v) =
-  let n, r = Vect.decomp_cst v in
+let cut isZ env rmin sol (rst : Restricted.t) (tbl:tableau) (x, v) =
+  let n, r = InfVect.decomp_cst v in
+  let (n,_)    = Inf.decomp n in (* Ignore epsilon part - for now *)
   let fn = frac_num (Q.abs n) in
   if fn =/ Q.zero then Forget (* The solution is integral *)
   else
@@ -651,7 +666,7 @@ let cut env rmin sol (rst : Restricted.t) tbl (x, v) =
       , make_farkas_proof env (Vect.normalise (cut_vector (snd ccoeff))) )
     in
     let check_cutting_plane (p, c) =
-      match WithProof.cutting_plane c with
+      match WithProof.cutting_plane_isz isZ c with
       | None ->
         if debug then
           Printf.printf "%s: This is not a cutting plane for %a\n%a:" p
@@ -698,10 +713,10 @@ let merge_best lt oldr newr =
     Z.zero v
  *)
 
-let find_cut nb env u sol rst tbl =
+let find_cut isZ nb env u (sol:qsolution)  rst (tbl:tableau) =
   if nb = 0 then
     IMap.fold
-      (fun x v acc -> merge_result_old acc (cut env u sol rst tbl) (x, v))
+      (fun x v acc -> merge_result_old acc (cut isZ env u sol rst tbl) (x, v))
       tbl Forget
   else
     let lt (_, wp1) (_, wp2) =
@@ -709,27 +724,27 @@ let find_cut nb env u sol rst tbl =
       ProofFormat.pr_size (WithProof.proof wp1) </ ProofFormat.pr_size  (WithProof.proof wp2)
     in
     IMap.fold
-      (fun x v acc -> merge_best lt acc (cut env u sol rst tbl (x, v)))
+      (fun x v acc -> merge_best lt acc (cut isZ env u sol rst tbl (x, v)))
       tbl Forget
 
-let find_split env tbl rst =
+
+
+let find_split isZ env tbl rst =
   let is_split x v =
-    let v, n =
-      let n, _ = Vect.decomp_cst v in
-      if Restricted.is_restricted x rst then
-        let n', v = Vect.decomp_cst @@ WithProof.polynomial @@ PrfEnv.find x env in
-        (v, n -/ n')
-      else (Vect.set x Q.one Vect.null, n)
-    in
+    (* Maybe we can cut over a restricted variable. TODO
+     *)
     if Restricted.is_restricted x rst then None
     else
-      let fn = frac_num n in
-      if fn =/ Q.zero then None
-      else
-        let fn = Q.abs fn in
-        let score = Q.min fn (Q.one -/ fn) in
-        let vect = Vect.add (Vect.cst (Q.neg n)) v in
-        Some (Vect.normalise vect, score)
+      let n , _ = InfVect.decomp_cst v in
+      match Inf.frac_num n with
+      | None -> None
+      | Some fn ->
+         let fn = Q.abs fn in
+         let score = Q.min fn (Q.one -/ fn) in
+         let vect = Vect.set x Q.one (Vect.cst (fst (Inf.decomp n))) in
+         if LinPoly.is_integer isZ vect then
+           Some (Vect.normalise vect, score)
+         else None
   in
   IMap.fold
     (fun x v acc ->
@@ -743,7 +758,7 @@ let find_split env tbl rst =
 
 let var_of_vect v = fst (fst (Vect.decomp_fst v))
 
-let eliminate_variable (bounded, env, tbl) x =
+let eliminate_variable (bounded, env, (tbl:tableau)) x =
   if debug then
     Printf.printf "Eliminating variable %a from tableau\n%a\n" LinPoly.pp_var x
       output_tableau tbl;
@@ -761,7 +776,7 @@ let eliminate_variable (bounded, env, tbl) x =
   let zp = WithProof.def z Ge zv in
   let tp = WithProof.def t Ge tv in
   (* Pivot the current tableau using xdef *)
-  let tbl = IMap.map (fun v -> Vect.subst x xdef v) tbl in
+  let tbl = IMap.map (fun v -> InfVect.subst x (InfVect.of_vect xdef false) v) tbl in
   (* Pivot the proof environment *)
   let env =
     PrfEnv.map
@@ -782,7 +797,7 @@ let eliminate_variable (bounded, env, tbl) x =
     Printf.printf "Environment\n %a\n" output_env env );
   (bounded, env, tbl)
 
-let integer_solver lp =
+let integer_solver isZ lp =
   let insert_row vr v rst tbl =
     match push_real true vr v rst tbl with
     | Sat (t', x) ->
@@ -813,7 +828,7 @@ let integer_solver lp =
         flush stdout
       end;
       if !nb mod 3 = 0 then
-        match find_split env tbl rst with
+        match find_split isZ env tbl rst with
         | None ->
           None (* There is no hope, there should be an integer solution *)
         | Some (v, s) -> (
@@ -831,7 +846,7 @@ let integer_solver lp =
             let v1', v2' = (WithProof.polynomial wp1, WithProof.polynomial wp2) in
             if debug then
               Printf.fprintf stdout "Solving with %a\n" LinPoly.pp v1';
-            let res1 = insert_row vr v1' (Restricted.set_exc vr rst) tbl in
+            let res1 = insert_row vr (InfVect.of_vect v1' false) (Restricted.set_exc vr rst) tbl in
             let prf1 = isolve (IMap.add vr (WithProof.def v1' Ge vr) env) cr res1 in
             match prf1 with
             | None -> None
@@ -841,7 +856,7 @@ let integer_solver lp =
               else (
                 if debug then
                   Printf.fprintf stdout "Solving with %a\n" Vect.pp v2';
-                let res2 = insert_row vr v2' (Restricted.set_exc vr rst) tbl in
+                let res2 = insert_row vr (InfVect.of_vect v2' false) (Restricted.set_exc vr rst) tbl in
                 let prf2 =
                   isolve (IMap.add vr (WithProof.def v2' Ge vr) env) cr res2
                 in
@@ -849,24 +864,28 @@ let integer_solver lp =
                 | None -> None
                 | Some prf2 -> Some (Split (vr, v, prf1, prf2)) ) ) )
       else
-        let sol = find_full_solution rst tbl in
-        match find_cut (!nb mod 2) env cr (*x*) sol rst tbl with
+        let sol = find_q_solution rst tbl in
+        match find_cut isZ (!nb mod 2) env cr (*x*) sol rst tbl with
         | Forget ->
           None (* There is no hope, there should be an integer solution *)
         | Hit (cr, wp) -> (
           let (v, op), cut = WithProof.repr wp in
           let vr = LinPoly.MonT.get_fresh () in
           if op = Eq then
-            (* This is a contradiction *)
+            begin (* This is a contradiction *)
+            if debug then
+              Printf.fprintf stdout "Found a contradiction\n %a\n" WithProof.output wp;
             Some (Step (vr, CutPrf cut, Done))
-          else
-            let res = insert_row vr v (Restricted.set_exc vr rst) tbl in
+            end
+          else begin
+            if debug then Printf.fprintf stdout "Found a cut\n %a\n" WithProof.output wp;
+            let res = insert_row vr (InfVect.of_vect v false) (Restricted.set_exc vr rst) tbl in
             let prf =
               isolve (IMap.add vr (WithProof.def v op vr) env) (Some cr) res
             in
             match prf with
             | None -> None
-            | Some p -> Some (Step (vr, CutPrf cut, p)) )
+            | Some p -> Some (Step (vr, CutPrf cut, p)) end)
         | Keep (x, v) -> (
           if debug then
             Printf.fprintf stdout "Remove %a from Tableau\n" LinPoly.pp_var x;
@@ -876,7 +895,7 @@ let integer_solver lp =
                 if x <> 0 && not (Restricted.is_restricted x rst) then
                   eliminate_variable acc x
                 else acc)
-              (IMap.empty, env, tbl) v
+              (IMap.empty, env, tbl) (snd (InfVect.decomp_cst v))
           in
           let prf = isolve env cr (Inl (rst, tbl, None)) in
           match prf with
@@ -891,11 +910,11 @@ let integer_solver lp =
   let res = solve true l' (Restricted.make vr0) IMap.empty in
   isolve env None res
 
-let integer_solver lp =
+let integer_solver isZ lp =
   nb_pivot := 0;
   if debug then
     Printf.printf "Input integer solver\n%a\n" WithProof.output_sys lp;
-  match integer_solver lp with
+  match integer_solver isZ lp with
   | None ->
     profile_info := (false, !nb_pivot) :: !profile_info;
     None
diff --git a/plugins/micromega/simplex.mli b/plugins/micromega/simplex.mli
index 5854c36848e1..47dcd2ef6b76 100644
--- a/plugins/micromega/simplex.mli
+++ b/plugins/micromega/simplex.mli
@@ -9,7 +9,7 @@
 (************************************************************************)
 
 open Polynomial
-
+open Mutils
 (** Profiling *)
 
 type profile_info =
@@ -23,9 +23,10 @@ type profile_info =
 val get_profile_info : unit -> profile_info
 
 (** Simplex interface *)
+(*type solution = InfVect.Inf.t Int.Map.t
 
-val find_point : cstr list -> Vect.t option
+val find_point : cstr list -> solution option *)
 val find_unsat_certificate : cstr list -> Vect.t option
 
 val integer_solver :
-  WithProof.t list -> ProofFormat.proof option
+  ISet.t option -> WithProof.t list -> ProofFormat.proof option
diff --git a/plugins/micromega/vect.ml b/plugins/micromega/vect.ml
index 5c73fdc37744..6870d2fdcfe6 100644
--- a/plugins/micromega/vect.ml
+++ b/plugins/micromega/vect.ml
@@ -57,17 +57,11 @@ let pp_var_num pp_var o {var = v; coe = n} =
   else Printf.fprintf o "%s*%a" (Q.to_string n) pp_var v
 
 let pp_var_num_smt pp_var o {var = v; coe = n} =
-  let pp_num o q =
-    let nn = Q.num n in
-    let dn = Q.den n in
-    if Z.equal dn Z.one then output_string o (Z.to_string nn)
-    else Printf.fprintf o "(/ %s %s)" (Z.to_string nn) (Z.to_string dn)
-  in
-  if Int.equal v 0 then if Q.zero =/ n then () else pp_num o n
+  if Int.equal v 0 then if Q.zero =/ n then () else pp_smt_num o n
   else if Q.one =/ n then pp_var o v
   else if Q.minus_one =/ n then Printf.fprintf o "(- %a)" pp_var v
   else if Q.zero =/ n then ()
-  else Printf.fprintf o "(* %a %a)" pp_num n pp_var v
+  else Printf.fprintf o "(* %a %a)" pp_smt_num n pp_var v
 
 let rec pp_gen pp_var o v =
   match v with
@@ -200,12 +194,13 @@ let decomp_fst v =
 
 let rec subst (vr : int) (e : t) (v : t) =
   match v with
-  | [] -> []
+  | [] -> (Q.zero,[])
   | {var = x; coe = n} :: v' -> (
     match Int.compare vr x with
-    | 0 -> mul_add n e Q.one v'
-    | -1 -> v
-    | 1 -> add [{var = x; coe = n}] (subst vr e v')
+    | 0 -> (n, mul_add n e Q.one v')
+    | -1 -> (Q.zero, v)
+    | 1 -> let (q,res) = subst vr e v' in
+           (q, add [{var = x; coe = n}] res)
     | _ -> assert false )
 
 let fold f acc v = List.fold_left (fun acc x -> f acc x.var x.coe) acc v
@@ -261,6 +256,24 @@ let dotproduct v1 v2 =
   in
   dot Q.zero v1 v2
 
+module Classify =
+  struct
+
+    type t =
+      | IsCst of Q.t * Q.t * var  (* [[IsCst c a1 x1]] =  c + a1.x1 *)
+      | IsVar of Q.t * var * Q.t * var  (* [[IsVar a1 x1 a2 x2]] = a1.x1 + x2.x2 *)
+
+    let classify v =
+      match v with
+      | [{var = x; coe = v}] ->
+         if Int.equal x 0 then None else Some (IsCst (Q.zero,v,x))
+      | [{var = 0; coe = v}; {var = x; coe = v'}] ->
+         Some (IsCst (v,v',x))
+      | [{var= x1; coe =a1}; {var = x2;coe = a2}] ->
+         Some (IsVar(a1,x1,a2,x2))
+      |   _ -> None
+  end
+
 module Bound = struct
   type t = {cst : Q.t; var : var; coeff : Q.t}
 
diff --git a/plugins/micromega/vect.mli b/plugins/micromega/vect.mli
index c47f4355b0fd..739002e3712e 100644
--- a/plugins/micromega/vect.mli
+++ b/plugins/micromega/vect.mli
@@ -126,8 +126,8 @@ val mul : Q.t -> t -> t
 (** [mul_add c1 v1 c2 v2] returns the linear combination c1.v1+c2.v2 *)
 val mul_add : Q.t -> t -> Q.t -> t -> t
 
-(** [subst x v v'] replaces x by v in vector v' *)
-val subst : int -> t -> t -> t
+(** [subst x v v'] replaces x by v in vector v' and also returns the coefficient of x in v' *)
+val subst : int -> t -> t -> Q.t * t
 
 (** [div c1 v1] returns the mutiplication by the inverse of c1 i.e (1/c1).v1 *)
 val div : Q.t -> t -> t
@@ -163,3 +163,13 @@ module Bound : sig
   val of_vect : vector -> t option
   val to_vect : t -> vector
 end
+
+module Classify :sig
+
+  type t =
+    | IsCst of Q.t * Q.t * var  (* [[IsCst c a1 x1]] =  c + a1.x1 *)
+    | IsVar of Q.t * var * Q.t * var  (* [[IsVar a1 x1 a2 x2]] = a1.x1 + x2.x2 *)
+
+  val classify : vector -> t option
+
+end
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index dcb7672ff454..65b7bea069b1 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -23,20 +23,23 @@ let debug_zify = CDebug.create ~name:"zify" ()
 let zify str =
   EConstr.of_constr
     (UnivGen.constr_of_monomorphic_global (Global.env ())
-       (Rocqlib.lib_ref ("ZifyClasses." ^ str)))
+       (Rocqlib.lib_ref ("TifyClasses." ^ str)))
 
 (** classes *)
-let rocq_InjTyp = lazy (Rocqlib.lib_ref "ZifyClasses.InjTyp")
-
-let rocq_BinOp = lazy (Rocqlib.lib_ref "ZifyClasses.BinOp")
-let rocq_UnOp = lazy (Rocqlib.lib_ref "ZifyClasses.UnOp")
-let rocq_CstOp = lazy (Rocqlib.lib_ref "ZifyClasses.CstOp")
-let rocq_BinRel = lazy (Rocqlib.lib_ref "ZifyClasses.BinRel")
-let rocq_PropBinOp = lazy (Rocqlib.lib_ref "ZifyClasses.PropBinOp")
-let rocq_PropUOp = lazy (Rocqlib.lib_ref "ZifyClasses.PropUOp")
-let rocq_BinOpSpec = lazy (Rocqlib.lib_ref "ZifyClasses.BinOpSpec")
-let rocq_UnOpSpec = lazy (Rocqlib.lib_ref "ZifyClasses.UnOpSpec")
-let rocq_Saturate = lazy (Rocqlib.lib_ref "ZifyClasses.Saturate")
+let rocq_InjTyp = lazy (Rocqlib.lib_ref "TifyClasses.InjTyp")
+
+let rocq_BinOp = lazy (Rocqlib.lib_ref "TifyClasses.BinOp")
+let rocq_UnOp = lazy (Rocqlib.lib_ref "TifyClasses.UnOp")
+let rocq_CstOp = lazy (Rocqlib.lib_ref "TifyClasses.CstOp")
+let rocq_BinRel = lazy (Rocqlib.lib_ref "TifyClasses.BinRel")
+let rocq_PropBinOp = lazy (Rocqlib.lib_ref "TifyClasses.PropBinOp")
+let rocq_PropUOp = lazy (Rocqlib.lib_ref "TifyClasses.PropUOp")
+let rocq_BinOpSpec = lazy (Rocqlib.lib_ref "TifyClasses.BinOpSpec")
+let rocq_UnOpSpec = lazy (Rocqlib.lib_ref "TifyClasses.UnOpSpec")
+let rocq_Saturate = lazy (Rocqlib.lib_ref "TifyClasses.Saturate")
+
+(* Z *)
+let rocq_Z = lazy (Rocqlib.lib_ref "num.Z.type")
 
 (* morphism like lemma *)
 
@@ -85,11 +88,6 @@ let get_type_of env evd e =
 
 (* arguments are dealt with in a second step *)
 
-let rec find_option pred l =
-  match l with
-  | [] -> raise Not_found
-  | e :: l -> ( match pred e with Some r -> r | None -> find_option pred l )
-
 module ConstrMap = struct
   open Names.GlobRef
 
@@ -639,7 +637,7 @@ module MakeTable (E : Elt) : S = struct
   let safe_ref evd c =
     try
       fst (EConstr.destRef evd c)
-    with DestKO -> CErrors.user_err Pp.(str "Add Zify "++str E.name ++ str ": the term "++
+    with DestKO -> CErrors.user_err Pp.(str "Add Tify "++str E.name ++ str ": the term "++
                                           gl_pr_constr c ++ str " should be a global reference")
 
   let register_hint evd t elt =
@@ -772,7 +770,7 @@ let init_cache () =
 
 open EInjT
 
-(** Get constr of lemma and projections in ZifyClasses. *)
+(** Get constr of lemma and projections in TifyClasses. *)
 
 (** Module [CstrTable] records terms  [x] injected into [inj x]
     together with the corresponding type constraint.
@@ -1107,12 +1105,44 @@ let classify_prop env evd e =
   | _ -> OTHEROP (e, [||])
 
 
+
 let check_target_inj evd inj d =
   match inj , target_inj d with
   | None , _ -> true
   | Some _ , None -> false
   | Some i1 , Some i2 -> EInjT.eq_inj evd i1 i2
 
+type score =
+  | FullMatch
+  | PartialMatch
+  | NoMatch
+
+let le_score s1 s2 =
+  match s1, s2 with
+  | _ , FullMatch -> true
+  | FullMatch , _ -> false
+  | _   , PartialMatch -> true
+  | PartialMatch, _    -> false
+  | NoMatch , NoMatch  -> true
+
+
+let score_operator pref evd d =
+  match d with
+  | BinRel d -> if EConstr.eq_constr evd pref d.deriv.EBinRelT.target
+                then FullMatch else NoMatch
+  | BinOp d  -> begin
+     match EConstr.eq_constr evd pref d.deriv.EBinOpT.target1 ,
+           EConstr.eq_constr evd pref d.deriv.EBinOpT.target2 with
+         | false, false -> NoMatch
+         | false, true | true,false -> PartialMatch
+         | true , true -> FullMatch
+    end
+  | UnOp  d  ->
+     if EConstr.eq_constr evd pref d.deriv.EUnOpT.target1
+     then FullMatch else NoMatch
+  | CstOp d  -> FullMatch
+  |   _      -> FullMatch
+
 
 (** [match_operator env evd hd arg inj (t,d)]
      - hd is head operator of t
@@ -1120,33 +1150,58 @@ let check_target_inj evd inj d =
      - If t = Application _, then
        we extract the relevant number of arguments from arg
        and check for convertibility *)
-let match_operator env evd hd args inj (t, d) =
-  let decomp t i =
+let match_operator pref env evd hd args (inj: EInjT.t option) (t, d) =
+  let decomp s t i =
     let n = Array.length args in
     let t' = EConstr.mkApp (hd, Array.sub args 0 (n - i)) in
-    if is_convertible env evd t' t then Some (d, t) else None
+    if is_convertible env evd t' t then Some (s, (d, t)) else None
   in
 
   if check_target_inj evd inj d
   then
-  match t with
-  | OtherTerm t -> Some (d, t)
-  | Application t -> (
-    match d with
-    | CstOp _ -> decomp t 0
-    | UnOp _ -> decomp t 1
-    | BinOp _ -> decomp t 2
-    | BinRel _ -> decomp t 2
-    | PropOp _ -> decomp t 2
-    | PropUnOp _ -> decomp t 1
-    | _ -> None )
+    let s = score_operator pref evd d in
+    match t with
+    | OtherTerm t -> Some (s, (d, t))
+    | Application t ->
+       (match d with
+      | CstOp _ -> decomp s t 0
+      | UnOp _ -> decomp s t 1
+      | BinOp _ -> decomp s t 2
+      | BinRel _ -> decomp s t 2
+      | PropOp _ -> decomp s t 2
+      | PropUnOp _ -> decomp s t 1
+      | _ -> None )
   else None
 
+let find_best p l =
+
+  let best s r v =
+    match v with
+    | None -> Some(s,r)
+    | Some(s',r') -> if le_score s s'
+                     then v else Some(s,r) in
+  let get_result v =
+    match v with
+    | None -> raise Not_found
+    | Some(_,r) -> r in
+
+  let rec find res l =
+    match l with
+    | [] -> get_result res
+    | e::l -> match p e with
+              | None -> find res l
+              | Some(s',r') ->
+                 if s' = FullMatch then r'
+                 else  find (best s' r' res) l in
+  find None l
+
+
+
 let pp_trans_expr env evd e res =
   debug_zify (fun () -> Pp.(str "\ntrans_expr " ++ pp_prf evd e.inj e.constr res));
   res
 
-let rec trans_expr env evd e =
+let rec trans_expr dtyp env evd e =
   let inj = e.inj in
   let e = e.constr in
   try
@@ -1154,8 +1209,8 @@ let rec trans_expr env evd e =
     if is_constant then evd, Term
     else
       let k, t =
-        find_option
-          (match_operator env evd c a (Some inj))
+        find_best
+          (match_operator dtyp env evd c a (Some inj))
           (ConstrMap.find_all evd c !table_cache)
       in
       let n = Array.length a in
@@ -1164,7 +1219,7 @@ let rec trans_expr env evd e =
         ECstOpT.(if c'.is_construct then evd, Term else evd, Prf (c'.cst, c'.cstinj))
       | UnOp {deriv = unop} ->
         let evd, prf =
-          trans_expr env evd
+          trans_expr dtyp env evd
             { constr = a.(n - 1)
             ; typ = unop.EUnOpT.source1
             ; inj = unop.EUnOpT.inj1_t }
@@ -1172,13 +1227,13 @@ let rec trans_expr env evd e =
         app_unop env evd e unop a.(n - 1) prf
       | BinOp {deriv = binop} ->
         let evd, prf1 =
-          trans_expr env evd
+          trans_expr dtyp env evd
             { constr = a.(n - 2)
             ; typ = binop.EBinOpT.source1
             ; inj = binop.EBinOpT.inj1 }
         in
         let evd, prf2 =
-          trans_expr env evd
+          trans_expr dtyp env evd
             { constr = a.(n - 1)
             ; typ = binop.EBinOpT.source2
             ; inj = binop.EBinOpT.inj2 }
@@ -1187,9 +1242,9 @@ let rec trans_expr env evd e =
       | d -> evd, mkvar evd inj e
   with Not_found | DestKO -> evd, mkvar evd inj e
 
-let trans_expr env evd e =
+let trans_expr dtyp env evd e =
   try
-    let evd, prf = trans_expr env evd e in
+    let evd, prf = trans_expr dtyp env evd e in
     evd, pp_trans_expr env evd e prf
   with Not_found ->
     raise
@@ -1286,33 +1341,33 @@ let trans_un_prop op_constr op_iff p1 prf1 =
       ( EConstr.mkApp (op_constr, [|p1'|])
       , EConstr.mkApp (op_iff, [|p1; p1'; prf|]) )
 
-let rec trans_prop env evd e =
+let rec trans_prop dtyp env evd e =
   match classify_prop env evd e with
   | BINOP ({op_constr; op_iff}, p1, p2) ->
-    let evd, prf1 = trans_prop env evd p1 in
-    let evd, prf2 = trans_prop env evd p2 in
+    let evd, prf1 = trans_prop dtyp env evd p1 in
+    let evd, prf2 = trans_prop dtyp env evd p2 in
     evd, trans_bin_prop op_constr op_iff p1 prf1 p2 prf2
   | UNOP ({op_constr; op_iff}, p1) ->
-    let evd, prf1 = trans_prop env evd p1 in
+    let evd, prf1 = trans_prop dtyp env evd p1 in
     evd, trans_un_prop op_constr op_iff p1 prf1
   | OTHEROP (c, a) -> (
     try
       let k, t =
-        find_option
-          (match_operator env evd c a None)
+        find_best
+          (match_operator dtyp env evd c a None)
           (ConstrMap.find_all evd c !table_cache)
       in
       let n = Array.length a in
       match k with
       | BinRel {decl = br; deriv = rop} ->
         let evd, a1 =
-          trans_expr env evd
+          trans_expr dtyp env evd
             { constr = a.(n - 2)
             ; typ = rop.EBinRelT.source
             ; inj = rop.EBinRelT.inj }
         in
         let evd, a2 =
-          trans_expr env evd
+          trans_expr dtyp env evd
             { constr = a.(n - 1)
             ; typ = rop.EBinRelT.source
             ; inj = rop.EBinRelT.inj }
@@ -1321,9 +1376,9 @@ let rec trans_prop env evd e =
       | _ -> evd, IProof
     with Not_found | DestKO -> evd, IProof )
 
-let trans_check_prop env evd t =
+let trans_check_prop dtyp env evd t =
   if is_prop env evd t then
-    let evd, p = trans_prop env evd t in
+    let evd, p = trans_prop dtyp env evd t in
     evd, Some p
   else evd, None
 
@@ -1331,11 +1386,11 @@ let get_hyp_typ = function
   | NamedDecl.LocalDef (h, _, ty) | NamedDecl.LocalAssum (h, ty) ->
     (h.Context.binder_name, EConstr.of_constr ty)
 
-let trans_hyps env evd l =
+let trans_hyps dtyp env evd l =
   List.fold_left
     (fun (evd, acc) decl ->
       let h, ty = get_hyp_typ decl in
-      match trans_check_prop env evd ty with
+      match trans_check_prop dtyp env evd ty with
       | evd, None -> evd, acc
       | evd, Some p' -> evd, (h, ty, p') :: acc)
     (evd, []) l
@@ -1413,21 +1468,21 @@ let do_let tac (h : Constr.named_declaration) =
           let x = id.Context.binder_name in
           ignore
             (let eq = Lazy.force eq in
-             find_option
-               (match_operator env evd eq
+             find_best
+               (match_operator (* eq ??? *) eq env evd eq
                   [|EConstr.of_constr ty; EConstr.mkVar x; EConstr.of_constr t|] None)
                (ConstrMap.find_all evd eq !table_cache));
           tac x (EConstr.of_constr t) (EConstr.of_constr ty)
         with Not_found -> Tacticals.tclIDTAC)
 
-let iter_let_aux tac =
+let iter_let_aux  tac =
   Proofview.Goal.enter (fun gl ->
       let env = Tacmach.pf_env gl in
       let sign = Environ.named_context env in
       init_cache ();
-      Tacticals.tclMAP (do_let tac) sign)
+      Tacticals.tclMAP (do_let  tac) sign)
 
-let iter_let (tac : Ltac_plugin.Tacinterp.Value.t) =
+let iter_let  (tac : Ltac_plugin.Tacinterp.Value.t) =
   iter_let_aux (fun (id : Names.Id.t) t ty ->
       Ltac_plugin.Tacinterp.Value.apply tac
         [ Ltac_plugin.Tacinterp.Value.of_constr (EConstr.mkVar id)
@@ -1436,16 +1491,17 @@ let iter_let (tac : Ltac_plugin.Tacinterp.Value.t) =
 
 let elim_let = iter_let_aux elim_binding
 
-let zify_tac =
+
+let tify_op (ty:GlobRef.t) =
   Proofview.Goal.enter (fun gl ->
-      Rocqlib.check_required_library ["Stdlib"; "micromega"; "ZifyClasses"];
-      Rocqlib.check_required_library ["Stdlib"; "micromega"; "ZifyInst"];
+      Rocqlib.check_required_library ["Stdlib"; "micromega"; "TifyClasses"];
       init_cache ();
       let evd = Tacmach.project gl in
       let env = Tacmach.pf_env gl in
       let sign = Environ.named_context env in
-      let evd, concl = trans_check_prop env evd (Tacmach.pf_concl gl) in
-      let evd, hyps = trans_hyps env evd sign in
+      let dtyp   = EConstr.of_constr (UnivGen.constr_of_monomorphic_global env ty) in
+      let evd, concl = trans_check_prop dtyp env evd (Tacmach.pf_concl gl) in
+      let evd, hyps = trans_hyps dtyp env evd sign in
       let l = CstrTable.get () in
       Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd)
         (tclTHENOpt concl trans_concl
@@ -1454,6 +1510,8 @@ let zify_tac =
                  (List.rev_map (fun (h, p, t) -> trans_hyp h p t) hyps))
               (CstrTable.gen_cstr l))))
 
+let zify_op = fun () -> tify_op (Lazy.force rocq_Z)
+
 type pscript = Set of Names.Id.t * EConstr.t | Pose of Names.Id.t * EConstr.t
 
 type spec_env =
diff --git a/plugins/micromega/zify.mli b/plugins/micromega/zify.mli
index 30ae2100ccc5..607c8cbe15b2 100644
--- a/plugins/micromega/zify.mli
+++ b/plugins/micromega/zify.mli
@@ -26,7 +26,8 @@ module BinOpSpec : S
 module UnOpSpec : S
 module Saturate : S
 
-val zify_tac : unit Proofview.tactic
+val tify_op : Names.GlobRef.t -> unit Proofview.tactic
+val zify_op : unit -> unit Proofview.tactic
 val saturate : unit Proofview.tactic
 val iter_specs : unit Proofview.tactic
 val iter_let : Ltac_plugin.Tacinterp.Value.t -> unit Proofview.tactic