diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index c2866e3..3a509fc 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -17,6 +17,18 @@ jobs:
     strategy:
       matrix:
         image:
+          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.12.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.13.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.13'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.14'
+          - 'mathcomp/mathcomp:1.14.0-coq-8.15'
+          - 'mathcomp/mathcomp:1.14.0-coq-dev'
+          - 'mathcomp/mathcomp-dev:coq-8.13'
+          - 'mathcomp/mathcomp-dev:coq-8.14'
+          - 'mathcomp/mathcomp-dev:coq-8.15'
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:
diff --git a/Makefile.coq.local b/Makefile.coq.local
index cf10a07..34aa873 100644
--- a/Makefile.coq.local
+++ b/Makefile.coq.local
@@ -1,2 +1,2 @@
 theories/ring.vo : theories/common.elpi theories/ring.elpi theories/field.elpi
-theories/lra.vo : theories/lra.elpi
+theories/lra.vo : theories/lra.elpi theories/compat815.elpi
diff --git a/coq-mathcomp-algebra-tactics.opam b/coq-mathcomp-algebra-tactics.opam
index 674ebe1..9a870ad 100644
--- a/coq-mathcomp-algebra-tactics.opam
+++ b/coq-mathcomp-algebra-tactics.opam
@@ -23,7 +23,7 @@ ring/field expressions before normalization to the Horner form."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.16"}
+  "coq" {>= "8.13"}
   "coq-mathcomp-ssreflect" {>= "1.12"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-zify" {>= "1.1.0"}
diff --git a/examples/lra_examples.v b/examples/lra_examples.v
index 70eff07..ba13a92 100644
--- a/examples/lra_examples.v
+++ b/examples/lra_examples.v
@@ -104,7 +104,7 @@ Proof.
 lra.
 Qed.
 
-Lemma test_rat_constant x : 0 <= x -> 1 / 3 * x <= 2^-1 * x.
+Lemma test_rat_constant x : 0 <= x -> 1 / 3%:R * x <= 2%:R^-1 * x.
 Proof.
 lra.
 Qed.
@@ -155,8 +155,8 @@ Lemma vcgen_25 (n m jt j it i : F) :
   1 * it + -(2%:R) * i + -(1%:R) = 0 ->
   1 * jt + -(2%:R) * j + -(1%:R) = 0 ->
   1 * n + -(10%:R) = 0 ->
-  0 <= -(4028%:R)  * i + 6222%:R * j + 705%:R * m + -(16674%:R) ->
-  0 <= -(418%:R) * i + 651%:R * j + 94 %:R * m + -(1866%:R) ->
+  0 <= (* -(4028%:R)  * i + *) 6222%:R * j + 705%:R * m + -(16674%:R) ->
+  0 <= -(418%:R) * i + 651%:R * j + 94 %:R * m (* + -(1866%:R) *) ->
   0 <= -(209%:R) * i + 302%:R * j + 47%:R * m + -(839%:R) ->
   0 <= -(1%:R) * i + 1 * j + -(1%:R) ->
   0 <= -(1%:R) * j + 1 * m + 0 ->
@@ -165,8 +165,9 @@ Lemma vcgen_25 (n m jt j it i : F) :
   0 <= 7%:R * j + 10%:R * m + -(74%:R) ->
   0 <= 18%:R * j + -(139%:R) * m + 1188%:R ->
   0 <= 1  * i + 0 ->
-  0 <= 121%:R  * i + 810%:R  * j + -(7465%:R) * m + 64350%:R ->
+  0 <= 121%:R  * i + 810%:R * j + -(7465%:R) * m + 64350%:R ->
   1 = -(2%:R) * i + it.
+  (* some constants commented out because they are very slow to parse *)
 Proof.
 move=> *.
 lra.
diff --git a/theories/compat815.elpi b/theories/compat815.elpi
new file mode 100644
index 0000000..20d2a10
--- /dev/null
+++ b/theories/compat815.elpi
@@ -0,0 +1,7 @@
+solve (goal _Ctx _Trigger _Type _Proof
+       [str Tac815, str Tac816, N, F, FQ, E, F'] as G) GL :-
+  coq.version _Str _Major Minor _Patch,
+  (if (Minor i< 16)
+     (coq.ltac.call Tac815 [N, FQ, E, F'] G GL)
+     (coq.ltac.call Tac816 [N, F, F'] G GL);
+   coq.ltac.fail 0).
diff --git a/theories/lra.elpi b/theories/lra.elpi
index 5df66f9..9b503c5 100644
--- a/theories/lra.elpi
+++ b/theories/lra.elpi
@@ -142,23 +142,28 @@ rfstr _ _ _ :- coq.ltac.fail _ "Cannot find a realDomainType".
 % - [In] is a term of type [V],
 % - [OutM] is a reified constant of type [MExpr V]
 % - [Out] is a reified constant of type [PExpr Q]
-pred quote.cstr i:term, i:term, o:term, o:term.
-quote.cstr V {{ GRing.zero lp:Z }} OutM Out :- ring->zmod V Z,
-  OutM = {{ @Internals.MEint lp:V Z0 }}, Out = {{ PEc (Qmake Z0 1) }}.
-quote.cstr V {{ GRing.one lp:V' }} OutM Out :- coq.unify-eq V V' ok,
-  OutM = {{ @Internals.MEint lp:V (Zpos 1) }}, Out = {{ PEc (Qmake 1 1) }}.
-quote.cstr V {{ @GRing.natmul lp:Z (GRing.one lp:V') lp:X }} OutM Out :-
+% - [OutQ] the reified [Out] as a [Q] (for <= 8.15 compat)
+pred quote.cstr i:term, i:term, o:term, o:term, o:term.
+quote.cstr V {{ GRing.zero lp:Z }} OutM Out OutQ :- ring->zmod V Z,
+  OutM = {{ @Internals.MEint lp:V Z0 }}, Out = {{ PEc (Qmake Z0 1) }},
+  OutQ = {{ Qmake Z0 1 }}.
+quote.cstr V {{ GRing.one lp:V' }} OutM Out OutQ :- coq.unify-eq V V' ok,
+  OutM = {{ @Internals.MEint lp:V (Zpos 1) }}, Out = {{ PEc (Qmake 1 1) }},
+  OutQ = {{ Qmake 1 1 }}.
+quote.cstr V {{ @GRing.natmul lp:Z (GRing.one lp:V') lp:X }} OutM Out OutQ :-
   ring->zmod V Z, coq.unify-eq V V' ok, nat->Z X XZ,
-  OutM = {{ @Internals.MEint lp:V lp:XZ }}, Out = {{ PEc (Qmake lp:XZ 1) }}.
+  OutM = {{ @Internals.MEint lp:V lp:XZ }}, Out = {{ PEc (Qmake lp:XZ 1) }},
+  OutQ = {{ Qmake lp:XZ 1 }}.
 
 % [quote.cstf V In OutM Out] reifies rational constants
 % - [V] is a [ringType] instance,
 % - [In] is a term of type [V],
 % - [OutM] is a reified constant of type [MExpr V]
 % - [Out] is a reified constant of type [PExpr Q]
-pred quote.cstf i:term, i:term, o:term, o:term.
+% - [OutQ] the reified [Out] as a [Q] (for <= 8.15 compat)
+pred quote.cstf i:term, i:term, o:term, o:term, o:term.
 quote.cstf V {{ @GRing.inv lp:U (@GRing.natmul lp:Z (GRing.one lp:V') lp:X) }}
-    OutM Out :- unitRing->ring U V, ring->zmod V Z, coq.unify-eq V V' ok,
+    OutM Out XQ :- unitRing->ring U V, ring->zmod V Z, coq.unify-eq V V' ok,
   nat->N X XN, XN = {{ Npos lp:XP }}, XQ = {{ Qmake 1 lp:XP }},
   field->unitRing F U,
   OutM = {{ @Internals.MErat lp:F lp:XQ }}, Out = {{ PEc lp:XQ }}.
@@ -169,109 +174,135 @@ quote.cstf V {{ @GRing.inv lp:U (@GRing.natmul lp:Z (GRing.one lp:V') lp:X) }}
 % - [In] is a term of type [V],
 % - [OutM] is a reified expression of type [MExpr V]
 % - [Out] is a reified expression of type [PExpr Q]
+% - [OutQ] the reified [Out] as a [Prop] about [Q] (for <= 8.15 compat)
 % - [VM] is a variable map, that is a list of terms of type [V].
-pred quote.expr i:term, i:(term -> term), i:term, o:term, o:term, o:list term.
-quote.expr V F {{ @GRing.add lp:Z lp:In1 lp:In2 }} OutM Out VM :-
+pred quote.expr i:term, i:(term -> term), i:term,
+    o:term, o:term, o:term, o:list term.
+quote.expr V F {{ @GRing.add lp:Z lp:In1 lp:In2 }} OutM Out OutQ VM :-
   ring->zmod V Z, !,
-  quote.expr V F In1 OutM1 Out1 VM, !, quote.expr V F In2 OutM2 Out2 VM, !,
+  quote.expr V F In1 OutM1 Out1 OutQ1 VM, !,
+  quote.expr V F In2 OutM2 Out2 OutQ2 VM, !,
   OutM = {{ @Internals.MEadd lp:V lp:OutM1 lp:OutM2 }},
-  Out = {{ PEadd lp:Out1 lp:Out2 }}.
-quote.expr V F {{ @GRing.mul lp:V' lp:In1 lp:In2 }} OutM Out VM :-
+  Out = {{ PEadd lp:Out1 lp:Out2 }},
+  OutQ = {{ (lp:OutQ1 + lp:OutQ2)%Q }}.
+quote.expr V F {{ @GRing.mul lp:V' lp:In1 lp:In2 }} OutM Out OutQ VM :-
   coq.unify-eq V V' ok, !,
-  quote.expr V F In1 OutM1 Out1 VM, !, quote.expr V F In2 OutM2 Out2 VM, !,
+  quote.expr V F In1 OutM1 Out1 OutQ1 VM, !,
+  quote.expr V F In2 OutM2 Out2 OutQ2 VM, !,
   OutM = {{ @Internals.MEmul lp:V lp:OutM1 lp:OutM2 }},
-  Out = {{ PEmul lp:Out1 lp:Out2 }}.
-quote.expr V F {{ @GRing.opp lp:Z lp:In1 }} OutM Out VM :-
+  Out = {{ PEmul lp:Out1 lp:Out2 }},
+  OutQ = {{ (lp:OutQ1 * lp:OutQ2)%Q }}.
+quote.expr V F {{ @GRing.opp lp:Z lp:In1 }} OutM Out OutQ VM :-
   ring->zmod V Z, !,
-  quote.expr V F In1 OutM1 Out1 VM, !,
-  OutM = {{ @Internals.MEopp lp:V lp:OutM1 }}, Out = {{ PEopp lp:Out1 }}.
-quote.expr V F {{ @GRing.exp lp:V' lp:In1 lp:X }} OutM Out VM :-
+  quote.expr V F In1 OutM1 Out1 OutQ1 VM, !,
+  OutM = {{ @Internals.MEopp lp:V lp:OutM1 }}, Out = {{ PEopp lp:Out1 }},
+  OutQ = {{ (- lp:OutQ1)%Q }}.
+quote.expr V F {{ @GRing.exp lp:V' lp:In1 lp:X }} OutM Out OutQ VM :-
   coq.unify-eq V V' ok, nat->N X XN, !,
-  quote.expr V F In1 OutM1 Out1 VM, !,
+  quote.expr V F In1 OutM1 Out1 OutQ1 VM, !,
   OutM = {{ @Internals.MEpow lp:V lp:OutM1 lp:XN }},
-  Out = {{ PEpow lp:Out1 lp:XN }}.
-quote.expr V _ In OutM Out _ :- quote.cstr V In OutM Out.
-quote.expr V _ In OutM Out _ :- field-mode, quote.cstf V In OutM Out.
-quote.expr V F In {{ @Internals.MEmorph lp:U lp:V lp:G lp:OutM }} Out VM :-
+  Out = {{ PEpow lp:Out1 lp:XN }},
+  nat->Z X XZ, OutQ = {{ (lp:OutQ1 ^ lp:XZ)%Q }}.
+quote.expr V _ In OutM Out OutQ _ :- quote.cstr V In OutM Out OutQ.
+quote.expr V _ In OutM Out OutQ _ :- field-mode, quote.cstf V In OutM Out OutQ.
+quote.expr V F In {{ @Internals.MEmorph lp:U lp:V lp:G lp:OutM }} Out OutQ VM :-
   coq.unify-eq
     {{ @GRing.RMorphism.apply lp:U lp:V lp:Ph lp:G lp:In1 }} In ok, !,
   quote.expr U (x\ F {{ @GRing.RMorphism.apply lp:U lp:V lp:Ph lp:G lp:x }})
-    In1 OutM Out VM.
-quote.expr V F In {{ @Internals.MEX lp:V lp:In }} {{ PEX lp:N }} VM :- !,
-  mem VM (F In) N.
+    In1 OutM Out OutQ VM.
+quote.expr V F In {{ @Internals.MEX lp:V lp:In }} {{ PEX lp:N }} OutQ VM :- !,
+  FIn = F In,
+  mem VM FIn N,
+  OutQ = {{ @Internals.R2Q lp:V lp:FIn }}.
 
 % [quote.exprw F In OutM Out VM] reifies arithmetic expressions
 % - [F] is a [realDomainType] or [realFieldType] instance,
 % - [In] is a term of type [F],
 % - [OutM] is a reified expression of type [MExpr F]
 % - [Out] is a reified expression of type [PExpr Q]
+% - [OutQ] the reified [Out] as a [Prop] about [Q] (for <= 8.15 compat)
 % - [VM] is a variable map, that is a list of terms of type [F].
-pred quote.exprw i:rf, i:term, o:term, o:term, o:list term.
-quote.exprw F In OutM Out VM :- F = field _, !,
-  field-mode => quote.expr { rf->ring F } (x\ x) In OutM Out VM.
-quote.exprw F In OutM Out VM :- F = ring _, !,
-  quote.expr { rf->ring F } (x\ x) In OutM Out VM.
+pred quote.exprw i:rf, i:term, o:term, o:term, o:term, o:list term.
+quote.exprw F In OutM Out OutQ VM :- F = field _, !,
+  field-mode => quote.expr { rf->ring F } (x\ x) In OutM Out OutQ VM.
+quote.exprw F In OutM Out OutQ VM :- F = ring _, !,
+  quote.expr { rf->ring F } (x\ x) In OutM Out OutQ VM.
 
 % [quote.bop2 F In OutM Out VM] reifies boolean (in)equalities
 % - [F] is a [realDomainType] or [realFieldType] instance,
 % - [In] is a term of type [bool],
 % - [OutM] is a reified expression of type [MFormula]
 % - [Out] is a reified expression of type [Formula Q]
+% - [OutQ] the reified [Out] as a [Prop] about [Q] (for <= 8.15 compat)
 % - [VM] is a variable map, that is a list of terms of type [F].
-pred quote.bop2 i:rf, i:term, o:term, o:term, o:list term.
-quote.bop2 F {{ @Order.le _ lp:O lp:X lp:Y }} OutM Out VM :- rf->porder F O, !,
-  quote.exprw F X XM' X' VM, !, quote.exprw F Y YM' Y' VM, !,
+pred quote.bop2 i:rf, i:term, o:term, o:term, o:term, o:list term.
+quote.bop2 F {{ @Order.le _ lp:O lp:X lp:Y }} OutM Out OutQ VM :-
+  rf->porder F O, !,
+  quote.exprw F X XM' X' XQ' VM, !, quote.exprw F Y YM' Y' YQ' VM, !,
   OutM = {{ Internals.Build_MFormula lp:XM' OpLe lp:YM' }},
-  Out = {{ Build_Formula lp:X' OpLe lp:Y' }}.
-quote.bop2 F {{ @Order.lt _ lp:O lp:X lp:Y }} OutM Out VM :- rf->porder F O, !,
-  quote.exprw F X XM' X' VM, !, quote.exprw F Y YM' Y' VM, !,
+  Out = {{ Build_Formula lp:X' OpLe lp:Y' }},
+  OutQ = {{ (lp:XQ' <= lp:YQ')%Q }}.
+quote.bop2 F {{ @Order.lt _ lp:O lp:X lp:Y }} OutM Out OutQ VM :-
+  rf->porder F O, !,
+  quote.exprw F X XM' X' XQ' VM, !, quote.exprw F Y YM' Y' YQ' VM, !,
   OutM = {{ Internals.Build_MFormula lp:XM' OpLt lp:YM' }},
-  Out = {{ Build_Formula lp:X' OpLt lp:Y' }}.
-quote.bop2 F {{ @eqtype.eq_op lp:T lp:X lp:Y) }} OutM Out VM :- rf->eq F T, !,
-  quote.exprw F X XM' X' VM, !, quote.exprw F Y YM' Y' VM, !,
+  Out = {{ Build_Formula lp:X' OpLt lp:Y' }},
+  OutQ = {{ (lp:XQ' < lp:YQ')%Q }}.
+quote.bop2 F {{ @eqtype.eq_op lp:T lp:X lp:Y) }} OutM Out OutQ VM :-
+  rf->eq F T, !,
+  quote.exprw F X XM' X' XQ' VM, !, quote.exprw F Y YM' Y' YQ' VM, !,
   OutM = {{ Internals.Build_MFormula lp:XM' OpEq lp:YM' }},
-  Out = {{ Build_Formula lp:X' OpEq lp:Y' }}.
+  Out = {{ Build_Formula lp:X' OpEq lp:Y' }},
+  OutQ = {{ (lp:XQ' == lp:YQ')%Q }}.
 
 % [quote.pop2 F In OutM Out VM] reifies (in)equalities of type Prop
 % - [F] is a [realDomainType] or [realFieldType] instance,
 % - [In] is a term of type [Prop],
 % - [OutM] is a reified expression of type [MFormula]
 % - [Out] is a reified expression of type [Formula Q]
+% - [OutQ] the reified [Out] as a [Prop] about [Q] (for <= 8.15 compat)
 % - [VM] is a variable map, that is a list of terms of type [F].
-pred quote.pop2 i:rf, i:term, o:term, o:term, o:list term.
-quote.pop2 F {{ is_true lp:E }} OutM Out VM :- quote.bop2 F E OutM Out VM.
-quote.pop2 F {{ @eq lp:T lp:X lp:Y) }} OutM Out VM :- rf->sort F T, !,
-  quote.exprw F X XM' X' VM, !, quote.exprw F Y YM' Y' VM, !,
+pred quote.pop2 i:rf, i:term, o:term, o:term, o:term, o:list term.
+quote.pop2 F {{ is_true lp:E }} OutM Out OutQ VM :-
+  quote.bop2 F E OutM Out OutQ VM.
+quote.pop2 F {{ @eq lp:T lp:X lp:Y) }} OutM Out OutQ VM :- rf->sort F T, !,
+  quote.exprw F X XM' X' XQ' VM, !, quote.exprw F Y YM' Y' YQ' VM, !,
   OutM = {{ Internals.Build_MFormula lp:XM' OpEq lp:YM' }},
-  Out = {{ Build_Formula lp:X' OpEq lp:Y' }}.
+  Out = {{ Build_Formula lp:X' OpEq lp:Y' }},
+  OutQ = {{ (lp:XQ' == lp:YQ')%Q }}.
 
 % [quote.bool F In OutM Out VM] reifies boolean formulas
 % - [F] is a [realDomainType] or [realFieldType] instance,
 % - [In] is a term of type [bool],
 % - [OutM] is a reified formula of type [BFormula MFormula Tauto.isBool]
 % - [Out] is a reified formula of type [BFormula (Formula Q) Tauto.isBool]
+% - [OutQ] the reified [Out] as a [Prop] about [Q] (for <= 8.15 compat)
 % - [VM] is a variable map, that is a list of terms of type [F].
-pred quote.bool i:rf, i:term, o:term, o:term, o:list term.
-quote.bool F {{ lp:F1 ==> lp:F2 }} OutM Out VM :- !,
-  quote.bool F F1 OutM1 Out1 VM, !, quote.bool F F2 OutM2 Out2 VM, !,
+pred quote.bool i:rf, i:term, o:term, o:term, o:term, o:list term.
+quote.bool F {{ lp:F1 ==> lp:F2 }} OutM Out OutQ VM :- !,
+  quote.bool F F1 OutM1 Out1 OutQ1 VM, !, quote.bool F F2 OutM2 Out2 OutQ2 VM,
   OutM = {{ IMPL lp:OutM1 None lp:OutM2 }},
-  Out = {{ IMPL lp:Out1 None lp:Out2 }}.
-quote.bool F {{ lp:F1 && lp:F2 }} OutM Out VM :- !,
-  quote.bool F F1 OutM1 Out1 VM, !, quote.bool F F2 OutM2 Out2 VM, !,
-  OutM = {{ AND lp:OutM1 lp:OutM2 }}, Out = {{ AND lp:Out1 lp:Out2 }}.
-quote.bool F {{ lp:F1 || lp:F2 }} OutM Out VM :- !,
-  quote.bool F F1 OutM1 Out1 VM, !, quote.bool F F2 OutM2 Out2 VM, !,
-  OutM = {{ OR lp:OutM1 lp:OutM2 }}, Out = {{ OR lp:Out1 lp:Out2 }}.
-quote.bool F {{ ~~ lp:F1 }} OutM Out VM :- !, quote.bool F F1 OutM1 Out1 VM, !,
-  OutM = {{ NOT lp:OutM1 }}, Out = {{ NOT lp:Out1 }}.
-quote.bool _ {{ true }} OutM Out _ :- !,
-  OutM = {{ TT Tauto.isBool }}, Out = {{ TT Tauto.isBool }}.
-quote.bool _ {{ false }} OutM Out _ :- !,
-  OutM = {{ FF Tauto.isBool }}, Out = {{ FF Tauto.isBool }}.
-quote.bool F In OutM Out VM :- quote.bop2 F In OutM' Out' VM,
+  Out = {{ IMPL lp:Out1 None lp:Out2 }},
+  OutQ = {{ lp:OutQ1 -> lp:OutQ2 }}.
+quote.bool F {{ lp:F1 && lp:F2 }} OutM Out OutQ VM :- !,
+  quote.bool F F1 OutM1 Out1 OutQ1 VM, !, quote.bool F F2 OutM2 Out2 OutQ2 VM,
+  OutM = {{ AND lp:OutM1 lp:OutM2 }}, Out = {{ AND lp:Out1 lp:Out2 }},
+  OutQ = {{ lp:OutQ1 /\ lp:OutQ2 }}.
+quote.bool F {{ lp:F1 || lp:F2 }} OutM Out OutQ VM :- !,
+  quote.bool F F1 OutM1 Out1 OutQ1 VM, !, quote.bool F F2 OutM2 Out2 OutQ2 VM,
+  OutM = {{ OR lp:OutM1 lp:OutM2 }}, Out = {{ OR lp:Out1 lp:Out2 }},
+  OutQ = {{ lp:OutQ1 \/ lp:OutQ2 }}.
+quote.bool F {{ ~~ lp:F1 }} OutM Out OutQ VM :- !,
+  quote.bool F F1 OutM1 Out1 OutQ1 VM, !,
+  OutM = {{ NOT lp:OutM1 }}, Out = {{ NOT lp:Out1 }}, OutQ = {{ ~ lp:OutQ1 }}.
+quote.bool _ {{ true }} OutM Out OutQ _ :- !,
+  OutM = {{ TT Tauto.isBool }}, Out = {{ TT Tauto.isBool }}, OutQ = {{ True }}.
+quote.bool _ {{ false }} OutM Out OutQ _ :- !,
+  OutM = {{ FF Tauto.isBool }}, Out = {{ FF Tauto.isBool }}, OutQ = {{ False }}.
+quote.bool F In OutM Out OutQ VM :- quote.bop2 F In OutM' Out' OutQ VM,
   OutM = {{ A Tauto.isBool lp:OutM' tt }},
   Out = {{ A Tauto.isBool lp:Out' tt }}.
-quote.bool _ In OutM Out _ :-
+quote.bool _ In OutM Out In _ :-
   OutM = {{ X Tauto.isBool lp:In }}, Out = {{ X Tauto.isBool lp:In }}.
 
 % [quote.prop F In OutM Out VM] reifies formulas of type Prop
@@ -279,38 +310,46 @@ quote.bool _ In OutM Out _ :-
 % - [In] is a term of type [Prop],
 % - [OutM] is a reified formula of type [BFormula MFormula Tauto.isProp]
 % - [Out] is a reified formula of type [BFormula (Formula Q) Tauto.isProp]
+% - [OutQ] the reified [Out] as a [Prop] about [Q] (for <= 8.15 compat)
 % - [VM] is a variable map, that is a list of terms of type [F].
-pred quote.prop i:rf, i:term, o:term, o:term, o:list term.
-quote.prop F {{ lp:F1 -> lp:F2 }} OutM Out VM :- !,
-  quote.prop F F1 OutM1 Out1 VM, !, quote.prop F F2 OutM2 Out2 VM, !,
+pred quote.prop i:rf, i:term, o:term, o:term, o:term, o:list term.
+quote.prop F {{ lp:F1 -> lp:F2 }} OutM Out OutQ VM :- !,
+  quote.prop F F1 OutM1 Out1 OutQ1 VM, !, quote.prop F F2 OutM2 Out2 OutQ2 VM,
   OutM = {{ IMPL lp:OutM1 None lp:OutM2 }},
-  Out = {{ IMPL lp:Out1 None lp:Out2 }}.
-quote.prop F {{ iff lp:F1 lp:F2 }} OutM Out VM :- !,
-  quote.prop F F1 OutM1 Out1 VM, !, quote.prop F F2 OutM2 Out2 VM, !,
-  OutM = {{ IFF lp:OutM1 lp:OutM2 }}, Out = {{ IFF lp:Out1 lp:Out2 }}.
-quote.prop F {{ lp:F1 /\ lp:F2 }} OutM Out VM :- !,
-  quote.prop F F1 OutM1 Out1 VM, !, quote.prop F F2 OutM2 Out2 VM, !,
-  OutM = {{ AND lp:OutM1 lp:OutM2 }}, Out = {{ AND lp:Out1 lp:Out2 }}.
-quote.prop F {{ lp:F1 \/ lp:F2 }} OutM Out VM :- !,
-  quote.prop F F1 OutM1 Out1 VM, !, quote.prop F F2 OutM2 Out2 VM, !,
-  OutM = {{ OR lp:OutM1 lp:OutM2 }}, Out = {{ OR lp:Out1 lp:Out2 }}.
-quote.prop F {{ ~ lp:F1 }} OutM Out VM :- !, quote.prop F F1 OutM1 Out1 VM, !,
-  OutM = {{ NOT lp:OutM1 }}, Out = {{ NOT lp:Out1 }}.
-quote.prop _ {{ True }} OutM Out _ :- !,
-  OutM = {{ TT Tauto.isProp }}, Out = {{ TT Tauto.isProp }}.
-quote.prop _ {{ False }} OutM Out _ :- !,
-  OutM = {{ FF Tauto.isProp }}, Out = {{ FF Tauto.isProp }}.
-quote.prop F {{ is_true lp:In1 }} OutM Out VM :- !,
-  quote.bool F In1 OutM1 Out1 VM, !,
+  Out = {{ IMPL lp:Out1 None lp:Out2 }},
+  OutQ = {{ lp:OutQ1 -> lp:OutQ2 }}.
+quote.prop F {{ iff lp:F1 lp:F2 }} OutM Out OutQ VM :- !,
+  quote.prop F F1 OutM1 Out1 OutQ1 VM, !, quote.prop F F2 OutM2 Out2 OutQ2 VM,
+  OutM = {{ IFF lp:OutM1 lp:OutM2 }}, Out = {{ IFF lp:Out1 lp:Out2 }},
+  OutQ = {{ iff lp:OutQ1 lp:OutQ2 }}.
+quote.prop F {{ lp:F1 /\ lp:F2 }} OutM Out OutQ VM :- !,
+  quote.prop F F1 OutM1 Out1 OutQ1 VM, !, quote.prop F F2 OutM2 Out2 OutQ2 VM,
+  OutM = {{ AND lp:OutM1 lp:OutM2 }}, Out = {{ AND lp:Out1 lp:Out2 }},
+  OutQ = {{ lp:OutQ1 /\ lp:OutQ2 }}.
+quote.prop F {{ lp:F1 \/ lp:F2 }} OutM Out OutQ VM :- !,
+  quote.prop F F1 OutM1 Out1 OutQ1 VM, !, quote.prop F F2 OutM2 Out2 OutQ2 VM,
+  OutM = {{ OR lp:OutM1 lp:OutM2 }}, Out = {{ OR lp:Out1 lp:Out2 }},
+  OutQ = {{ lp:OutQ1 \/ lp:OutQ2 }}.
+quote.prop F {{ ~ lp:F1 }} OutM Out OutQ VM :- !,
+  quote.prop F F1 OutM1 Out1 OutQ1 VM, !,
+  OutM = {{ NOT lp:OutM1 }}, Out = {{ NOT lp:Out1 }}, OutQ = {{ ~ lp:OutQ1 }}.
+quote.prop _ {{ True }} OutM Out OutQ _ :- !,
+  OutM = {{ TT Tauto.isProp }}, Out = {{ TT Tauto.isProp }}, OutQ = {{ True }}.
+quote.prop _ {{ False }} OutM Out OutQ _ :- !,
+  OutM = {{ FF Tauto.isProp }}, Out = {{ FF Tauto.isProp }}, OutQ = {{ False }}.
+quote.prop F {{ is_true lp:In1 }} OutM Out OutQ VM :- !,
+  quote.bool F In1 OutM1 Out1 OutQ1 VM, !,
   OutM = {{ EQ lp:OutM1 (TT Tauto.isBool) }},
-  Out = {{ EQ lp:Out1 (TT Tauto.isBool) }}.
-quote.prop F {{ @eq bool lp:In1 lp:In2 }} OutM Out VM :- !,
-  quote.bool F In1 OutM1 Out1 VM, !, quote.bool F In2 OutM2 Out2 VM,
-  OutM = {{ EQ lp:OutM1 lp:OutM2 }}, Out = {{ EQ lp:Out1 lp:Out2 }}.
-quote.prop F In OutM Out VM :- quote.pop2 F In OutM' Out' VM,
+  Out = {{ EQ lp:Out1 (TT Tauto.isBool) }},
+  OutQ = {{ lp:OutQ1 }}.
+quote.prop F {{ @eq bool lp:In1 lp:In2 }} OutM Out OutQ VM :- !,
+  quote.bool F In1 OutM1 Out1 OutQ1 VM, !, quote.bool F In2 OutM2 Out2 OutQ2 VM,
+  OutM = {{ EQ lp:OutM1 lp:OutM2 }}, Out = {{ EQ lp:Out1 lp:Out2 }},
+  OutQ = {{ lp:OutQ1 <-> lp:OutQ2 }}.
+quote.prop F In OutM Out OutQ VM :- quote.pop2 F In OutM' Out' OutQ VM,
   OutM = {{ A Tauto.isProp lp:OutM' tt }},
   Out = {{ A Tauto.isProp lp:Out' tt }}.
-quote.prop _ In OutM Out _ :-
+quote.prop _ In OutM Out In _ :-
   OutM = {{ X Tauto.isProp lp:In }}, Out = {{ X Tauto.isProp lp:In }}.
 
 % [simplify.bool In Out] reduces a boolean formula to [X _]
@@ -368,10 +407,12 @@ simplify.prop X X.
 % - [In] is a term of type [Prop],
 % - [OutM] is a reified formula of type [BFormula MFormula Tauto.isProp]
 % - [Out] is a reified formula of type [BFormula (Formula Q) Tauto.isProp]
+% - [OutQ] the reified [Out] as a [Prop] about [Q] (for <= 8.15 compat)
 % - [VM] is a variable map, that is a list of terms of type [F].
-pred quote i:rf, i:term, o:term, o:term, o:list term.
-quote F In OutM' Out' VM :-
-  quote.prop F In OutM Out VM, simplify.prop OutM OutM', simplify.prop Out Out'.
+pred quote i:rf, i:term, o:term, o:term, o:term, o:list term.
+quote F In OutM' Out' OutQ VM :-
+  quote.prop F In OutM Out OutQ VM,
+  simplify.prop OutM OutM', simplify.prop Out Out'.
 
 % [quote.hyps F Hyps Goal ReifiedGoal Out ReifiedOut VM] reifies hypotheses
 % - [F] is a [realDomainType] or [realFieldType] instance,
@@ -379,26 +420,32 @@ quote F In OutM' Out' VM :-
 % - [Goal] is the goal, of type [Prop]
 % - [ReifiedGoalM] is the refied goal as a [BFormula MFormula Tauto.isProp]
 % - [ReifiedGoal] is the refied goal as a [BFormula (Formula Q) Tauto.isProp]
+% - [ReifiedGoalQ] the reified goal as a [Prop] about [Q] (for <= 8.15 compat)
 % - [Out] is a chain of implications including [Goal] and hypotheses in [Hyps]
 %   that have some arithmetic content
 % - [ReifiedOutM] is a reified version of [Out]
 %   as a [BFormula MFormula Tauto.isProp]
 % - [ReifiedOut] is a reified version of [Out]
 %   as a [BFormula (Formula Q) Tauto.isProp]
+% - [ReifiedOutQ] the [ReifiedOut] as a [Prop] about [Q] (for <= 8.15 compat)
 % - [VM] is a variable map, that is a list of terms of type [F].
-pred quote.hyps i:rf, i:list prop, i:term, i:term, i:term,
-  o:term, o:term, o:term, o:list term.
-quote.hyps F [decl _ _ H|Ctx] Type TypeFM TypeF Type'' TypeFM'' TypeF'' VM :-
-  quote F H HM' H' VM, not (H' = {{ X _ _ }}), !,
-  quote.hyps F Ctx Type TypeFM TypeF Type' TypeFM' TypeF' VM,
+pred quote.hyps i:rf, i:list prop, i:term, i:term, i:term, i:term,
+  o:term, o:term, o:term, o:term, o:list term.
+quote.hyps F [decl _ _ H|Ctx] Type TypeFM TypeF TypeFQ
+    Type'' TypeFM'' TypeF'' TypeFQ'' VM :-
+  quote F H HM' H' HQ' VM, not (H' = {{ X _ _ }}), !,
+  quote.hyps F Ctx Type TypeFM TypeF TypeFQ Type' TypeFM' TypeF' TypeFQ' VM,
   Type'' = {{ lp:H -> lp:Type' }},
   TypeFM'' = {{ IMPL lp:HM' None lp:TypeFM' }},
-  TypeF'' = {{ IMPL lp:H' None lp:TypeF' }}.
-quote.hyps F [decl _ _ _|Ctx] Type TypeFM TypeF Type' TypeFM' TypeF' VM :- !,
-  quote.hyps F Ctx Type TypeFM TypeF Type' TypeFM' TypeF' VM.
-quote.hyps F [def _ _ _ _|Ctx] Type TypeFM TypeF Type' TypeFM' TypeF' VM :- !,
-  quote.hyps F Ctx Type TypeFM TypeF Type' TypeFM' TypeF' VM.
-quote.hyps _ [] Type TypeFM TypeF Type TypeFM TypeF _.
+  TypeF'' = {{ IMPL lp:H' None lp:TypeF' }},
+  TypeFQ'' = {{ lp:HQ' -> lp:TypeFQ' }}.
+quote.hyps F [decl _ _ _|Ctx] Type TypeFM TypeF TypeFQ
+    Type' TypeFM' TypeF' TypeFQ' VM :- !,
+  quote.hyps F Ctx Type TypeFM TypeF TypeFQ Type' TypeFM' TypeF' TypeFQ' VM.
+quote.hyps F [def _ _ _ _|Ctx] Type TypeFM TypeF TypeFQ
+    Type' TypeFM' TypeF' TypeFQ' VM :- !,
+  quote.hyps F Ctx Type TypeFM TypeF TypeFQ Type' TypeFM' TypeF' TypeFQ' VM.
+quote.hyps _ [] Type TypeFM TypeF TypeFQ Type TypeFM TypeF TypeFQ _.
 
 % [exfalso_if_not_prop In Out Bool] changes [In] to [False]
 % when [In] is not a [Prop] (and then set [Bool] to [true])
@@ -414,13 +461,14 @@ exfalso_if_not_prop _ {{ False }} {{ true }}.
 % that are the names of the Ltac1 tactic to call respactively
 % in the [realFieldType] and [realDomainType] case and a third argument [N],
 % passed unchanged as first argument to the previous tactic.
-% The tactics [TacF] or [TacR] will receive six arguments:
+% The tactics [TacF] or [TacR] will receive seven arguments:
 % - [N] above
 % - [Efalso] a term of type [bool] indicating if the goal was changed to [False]
 % - [Type''] a term of type [Prop], an implication with the goal
 %   and selected hypotheses
 % - [TypeFM'] the reified [Type''] as a [BFormula MFormula Tauto.isProp]
 % - [TypeF'] the reified [Type''] as a [BFormula (Formula Q) Tauto.isProp]
+% - [TypeFQ'] the reified [Type''] as a [Prop] about [Q] (for <= 8.15 compat)
 % - [VM''] a variable map, giving the interpretation to variables in [TypeF']
 %   it is of type [VarMap.t F] where [F] is the carrier for the detected
 %   [realFieldType] or [realDomainType]
@@ -428,8 +476,9 @@ solve (goal Ctx _Trigger Type _Proof [str TacF, str TacR, N] as G) GL :-
   exfalso_if_not_prop Type Type' Efalso,
   std.rev Ctx Ctx', !,
   rfstr Ctx' Type' F, !,
-  quote F Type' TypeFM TypeF VM, !,
-  quote.hyps F Ctx' Type' TypeFM TypeF Type'' TypeFM' TypeF' VM, !,
+  quote F Type' TypeFM TypeF TypeFQ VM, !,
+  quote.hyps F Ctx' Type' TypeFM TypeF TypeFQ Type'' TypeFM' TypeF' TypeFQ' VM,
+  !,
   rf->numDomain F NDF,
   std.assert-ok!
     (coq.typecheck TypeFM' {{ BFormula (@Internals.MFormula lp:NDF) isProp }})
@@ -444,5 +493,6 @@ solve (goal Ctx _Trigger Type _Proof [str TacF, str TacR, N] as G) GL :-
     VM'',
   (if (F = field _) (Tac = TacF) (Tac = TacR)),
   (coq.ltac.call
-     Tac [N, trm Efalso, trm Type'', trm TypeFM', trm TypeF', trm VM''] G GL;
+     Tac [N, trm Efalso, trm Type'', trm TypeFM', trm TypeF', trm TypeFQ',
+          trm VM''] G GL;
    coq.ltac.fail 0).
diff --git a/theories/lra.v b/theories/lra.v
index ae72f84..93cb295 100644
--- a/theories/lra.v
+++ b/theories/lra.v
@@ -1,3 +1,4 @@
+From elpi Require Import elpi.
 Require Import DecimalNat DecimalPos List QArith.
 From Coq.micromega Require Import OrderedRing RingMicromega QMicromega EnvRing.
 From Coq.micromega Require Import Refl Tauto Lqa.
@@ -498,10 +499,11 @@ Fixpoint Pol_Q2Z (p : Pol Q) : Pol Z * positive := match p with
 Fixpoint Psatz_Q2Z (l : seq positive) (p : Psatz Q) : Psatz Z * positive :=
   match p with
   | PsatzC (Qmake n d) => (PsatzC n, d)
-  | PsatzLet p1 p2 =>
-      let (p1, n1) := Psatz_Q2Z l p1 in
-      let (p2, n2) := Psatz_Q2Z (n1 :: l) p2 in
-      (PsatzLet p1 p2, n2)
+  (* Add support for PsatzLet once 8.16 becomes the minimum Coq version *)
+  (* | PsatzLet p1 p2 => *)
+  (*     let (p1, n1) := Psatz_Q2Z l p1 in *)
+  (*     let (p2, n2) := Psatz_Q2Z (n1 :: l) p2 in *)
+  (*     (PsatzLet p1 p2, n2) *)
   | PsatzIn n => (PsatzIn _ n, nth 1%positive l n)
   | PsatzSquare p => let (p, n) := Pol_Q2Z p in (PsatzSquare p, Pos.mul n n)
   | PsatzMulC p1 p2 =>
@@ -517,17 +519,124 @@ Fixpoint Psatz_Q2Z (l : seq positive) (p : Psatz Q) : Psatz Z * positive :=
       let (p2, n2) := Psatz_Q2Z l p2 in
       let mulc c p := PsatzMulE (PsatzC (Zpos c)) p in
       (PsatzAdd (mulc n2 p1) (mulc n1 p2), Pos.mul n1 n2)
-  | PsatzZ => (PsatzZ _, 1%positive)
+  | _ => (PsatzZ _, 1%positive)
+  (* replace previous line by the following once 8.16 becomes the minimum Coq *)
+  (* | PsatzZ => (PsatzZ _, 1%positive) *)
   end.
 
 Definition seq_Psatz_Q2Z : seq (Psatz Q) -> seq (Psatz Z) :=
   map (fun p => fst (Psatz_Q2Z [::] p)).
 
+(* BEGIN compat Coq <= 8.15 *)
+(* This should be removed when algebra-tactics requires Coq >= 8.16
+   (also remove all the translation to Q in lra.elpi) *)
+
+(* Dummy function to feed micromega with formulas whose variables are in Q *)
+Definition R2Q {R : ringType} (_ : R) : Q := 0%Q.
+
+(* As a small optimization, micromega postprocesses formulas
+   to abstract parts that are not used in the proof.
+   In practice, algebraic parts of the formulas [A] are replaced
+   by propositions [X], see vcgen_25 in ../examples/lra_examples.v
+   for an example (most of the hypotheses are unused there).
+   We thus need to postprocess our own reified formulas to avoid
+   the witness produced by micromega to become out of sync. *)
+Let BF C k := BFormula (Formula C) k.
+Fixpoint abstract {C} (eval : forall k, BF C k -> rtyp k) {k} (aff : BF Q k) :
+    BF C k -> BF C k :=
+  match aff in GFormula k1 return BF C k1 -> BF C k1 with
+  | IMPL _ aff1 _ aff2
+  | AND _ aff1 aff2
+  | OR _ aff1 aff2
+  | IFF _ aff1 aff2 =>
+      fun ff =>
+        match
+          ff in GFormula k2
+          return (BF C k2 -> BF C k2) -> (BF C k2 -> BF C k2) -> BF C k2
+        with
+        | IMPL _ ff1 _ ff2 => fun a1 a2 => IMPL (a1 ff1) None (a2 ff2)
+        | AND _ ff1 ff2 => fun a1 a2 => AND (a1 ff1) (a2 ff2)
+        | OR _ ff1 ff2 => fun a1 a2 => OR (a1 ff1) (a2 ff2)
+        | IFF _ ff1 ff2 => fun a1 a2 => IFF (a1 ff1) (a2 ff2)
+        | TT _ => fun _ _ => TT _
+        | FF _ => fun _ _=> FF _
+        | X _ t => fun _ _ => X _ t
+        | A _ t a => fun _ _ => A _ t a
+        | NOT _ g2 => fun _ _ => NOT g2
+        | EQ g2 g3 => fun _ _ => EQ g2 g3
+        end (abstract eval aff1) (abstract eval aff2)
+  | X _ _ => fun ff => X _ (eval _ ff)
+  | TT _ | FF _ | A _ _ _ | NOT _ _ | EQ _ _ => id
+  end.
+
+(* Coq < 8.16 *)
+Ltac tac_compat tac fQ eval f :=
+  match eval hnf in (ltac:(tac) : fQ) with
+  | QTautoChecker_sound ?aff ?wit _ _ =>
+      let iaff := fresh "__aff" in
+      let iff := fresh "__ff" in
+      let iwit := fresh "__wit" in
+      pose (iaff := aff);
+      pose (iff := abstract eval iaff f);
+      pose (iwit := wit)
+  end.
+
+(* Coq >= 8.16 *)
+Ltac tac_ltac1 tac ff f :=
+  let iff := fresh "__ff" in
+  let iwit := fresh "__wit" in
+  pose (iff := f);
+  tac iwit ff.
+
+Ltac wlra_Q_compat _ := tac_compat lra.
+
+(* The tactic notation wlra_Q doesn't exist in Coq < 8.16, we thus declare
+   a tactic with the same name to avoid compilation errors
+   (this doesn't mask the tactic notation when it exists). *)
+Set Warnings "-unusable-identifier".
+Ltac wlra_Q w f := idtac.
+Set Warnings "unusable-identifier".
+Ltac wlra_Q_ltac1 _ := let wlra_Q w f := wlra_Q w f in tac_ltac1 wlra_Q.
+
+Ltac wnra_Q_compat _ := tac_compat nra.
+
+Set Warnings "-unusable-identifier".
+Ltac wnra_Q w f := idtac.
+Set Warnings "unusable-identifier".
+Ltac wnra_Q_ltac1 _ := let wnra_Q w f := wnra_Q w f in tac_ltac1 wnra_Q.
+
+Ltac wpsatz_Q_compat n := let psatz := psatz Q n in tac_compat psatz.
+
+Set Warnings "-unusable-identifier".
+Ltac wsos_Q w f := idtac.
+Ltac wpsatz_Q n w f := idtac.
+Set Warnings "unusable-identifier".
+Ltac wpsatz_Q_ltac1 n :=
+  let psatz w f := wsos_Q w f || wpsatz_Q n w f in tac_ltac1 psatz.
+
 End Internals.
 
+Elpi Tactic compat815.
+Elpi Accumulate File "theories/compat815.elpi".
+Elpi Typecheck.
+
+(* Elpi will call the first or second tactic depending on Coq version *)
+Tactic Notation "wlra_Q" ident(w) constr(ff) constr(fQ) constr(env) constr(f) :=
+  elpi compat815 "Internals.wlra_Q_compat" "Internals.wlra_Q_ltac1"
+       0 ltac_term:(ff) ltac_term:(fQ) ltac_term:(env) ltac_term:(f).
+Tactic Notation "wnra_Q" ident(w) constr(ff) constr(fQ) constr(env) constr(f) :=
+  elpi compat815 "Internals.wnra_Q_compat" "Internals.wnra_Q_ltac1"
+       0 ltac_term:(ff) ltac_term:(fQ) ltac_term:(env) ltac_term:(f).
+Tactic Notation "wpsatz_Q" int_or_var(n)
+       ident(w) constr(ff) constr(fQ) constr(env) constr(f) :=
+  elpi compat815 "Internals.wpsatz_Q_compat" "Internals.wpsatz_Q_ltac1"
+       ltac_int:(n) ltac_term:(ff) ltac_term:(fQ) ltac_term:(env) ltac_term:(f).
+
+(* END compat Coq <= 8.15 *)
+
 (* Main tactics, called from the elpi parser (c.f., lra.elpi) *)
 
-Ltac tacF tac efalso hyps_goal rff ff varmap :=
+Ltac tacF tac efalso hyps_goal rff ff ffQ varmap :=
   match efalso with true => exfalso | _ => idtac end;
   (suff: hyps_goal by exact);
   let irff := fresh "__rff" in
@@ -536,21 +645,20 @@ Ltac tacF tac efalso hyps_goal rff ff varmap :=
   let iwit := fresh "__wit" in
   let iprf := fresh "__prf" in
   pose (irff := rff);
-  pose (iff := ff);
   pose (ivarmap := varmap);
-  tac iwit ff;
+  tac iwit ff ffQ
+      (eval_bf (Internals.Feval_formula (VarMap.find 0 ivarmap))) ff;
   pose (iprf := erefl true <: QTautoChecker iff iwit = true);
   change (eval_bf Internals.Meval_formula irff);
   rewrite Internals.Mnorm_bf_correct;
   change (eval_bf (Internals.Feval_formula (VarMap.find 0 ivarmap)) iff);
   exact (Internals.FTautoChecker_sound iprf (VarMap.find 0 ivarmap)).
-Ltac lraF n := let wlra_Q w f := wlra_Q w f in tacF wlra_Q.
-Ltac nraF n := let wnra_Q w f := wnra_Q w f in tacF wnra_Q.
+Ltac lraF n := let wlra_Q w ff fQ e f := wlra_Q w ff fQ e f in tacF wlra_Q.
+Ltac nraF n := let wnra_Q w ff fQ e f := wnra_Q w ff fQ e f in tacF wnra_Q.
 Ltac psatzF n :=
-  let sos_or_psatzn w f := wsos_Q w f || wpsatz_Q n w f in
-  tacF sos_or_psatzn.
+  let wpsatz_Q w ff fQ e f := wpsatz_Q n w ff fQ e f in tacF wpsatz_Q.
 
-Ltac tacR tac efalso hyps_goal rff ff varmap :=
+Ltac tacR tac efalso hyps_goal rff ff ffQ varmap :=
   match efalso with true => exfalso | _ => idtac end;
   (suff: hyps_goal by exact);
   let irff := fresh "__rff" in
@@ -561,9 +669,9 @@ Ltac tacR tac efalso hyps_goal rff ff varmap :=
   match eval vm_compute in (Internals.BFormula_Q2Z ff) with
   | Some ?f =>
       pose (irff := rff);
-      pose (iff := f);
       pose (ivarmap := varmap);
-      tac iwit ff;
+      tac iwit ff ffQ
+          (eval_bf (Internals.Reval_formula (VarMap.find 0 ivarmap))) f;
       let tr := Internals.seq_Psatz_Q2Z in
       pose (iprf := erefl true <: Internals.ZTautoChecker iff (tr iwit) = true);
       change (eval_bf Internals.Meval_formula irff);
@@ -572,13 +680,10 @@ Ltac tacR tac efalso hyps_goal rff ff varmap :=
       exact (Internals.RTautoChecker_sound iprf (VarMap.find 0 ivarmap))
   | _ => fail  (* should never happen, the parser only parses int constants *)
   end.
-Ltac lraR n := let wlra_Q w f := wlra_Q w f in tacR wlra_Q.
-Ltac nraR n := let wnra_Q w f := wnra_Q w f in tacR wnra_Q.
+Ltac lraR n := let wlra_Q w ff fQ e f := wlra_Q w ff fQ e f in tacR wlra_Q.
+Ltac nraR n := let wnra_Q w ff fQ e f := wnra_Q w ff fQ e f in tacR wnra_Q.
 Ltac psatzR n :=
-  let sos_or_psatzn w f := wsos_Q w f || wpsatz_Q n w f in
-  tacF sos_or_psatzn.
-
-From elpi Require Import elpi.
+  let wpsatz_Q w ff fQ e f := wpsatz_Q n w ff fQ e f in tacR wpsatz_Q.
 
 Elpi Tactic lra.
 Elpi Accumulate File "theories/lra.elpi".