From 9ea4f66f5a125554a8f58e26688af7a32b9f221a Mon Sep 17 00:00:00 2001
From: Pierre Roux <pierre.roux@onera.fr>
Date: Fri, 24 Apr 2026 14:38:25 +0200
Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21849

---
 theories/ordered_qelim.v | 30 +++++++++++++++---------------
 theories/qe_rcf.v        | 22 +++++++++++-----------
 2 files changed, 26 insertions(+), 26 deletions(-)

diff --git a/theories/ordered_qelim.v b/theories/ordered_qelim.v
index 38f8689..98e9ac6 100644
--- a/theories/ordered_qelim.v
+++ b/theories/ordered_qelim.v
@@ -79,21 +79,21 @@ Declare Scope oterm_scope.
 Bind Scope oterm_scope with term.
 Bind Scope oterm_scope with formula.
 Delimit Scope oterm_scope with oT.
-Arguments Add _ _%oT _%oT.
-Arguments Opp _ _%oT.
-Arguments NatMul _ _%oT _%N.
-Arguments Mul _ _%oT _%oT.
-Arguments Mul _ _%oT _%oT.
-Arguments Inv _ _%oT.
-Arguments Exp _ _%oT _%N.
-Arguments Equal _ _%oT _%oT.
-Arguments Unit _ _%oT.
-Arguments And _ _%oT _%oT.
-Arguments Or _ _%oT _%oT.
-Arguments Implies _ _%oT _%oT.
-Arguments Not _ _%oT.
-Arguments Exists _ _%N _%oT.
-Arguments Forall _ _%N _%oT.
+Arguments Add _ _%_oT _%_oT.
+Arguments Opp _ _%_oT.
+Arguments NatMul _ _%_oT _%_N.
+Arguments Mul _ _%_oT _%_oT.
+Arguments Mul _ _%_oT _%_oT.
+Arguments Inv _ _%_oT.
+Arguments Exp _ _%_oT _%_N.
+Arguments Equal _ _%_oT _%_oT.
+Arguments Unit _ _%_oT.
+Arguments And _ _%_oT _%_oT.
+Arguments Or _ _%_oT _%_oT.
+Arguments Implies _ _%_oT _%_oT.
+Arguments Not _ _%_oT.
+Arguments Exists _ _%_N _%_oT.
+Arguments Forall _ _%_N _%_oT.
 
 Arguments Bool [T].
 Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not.
diff --git a/theories/qe_rcf.v b/theories/qe_rcf.v
index 41dfd0d..a65a9d6 100644
--- a/theories/qe_rcf.v
+++ b/theories/qe_rcf.v
@@ -98,17 +98,17 @@ Declare Scope qf_scope.
 Bind Scope qf_scope with term.
 Bind Scope qf_scope with formula.
 Delimit Scope qf_scope with qfT.
-Arguments Add _ _%qfT _%qfT.
-Arguments Opp _ _%qfT.
-Arguments NatMul _ _%qfT _%N.
-Arguments Mul _ _%qfT _%qfT.
-Arguments Mul _ _%qfT _%qfT.
-Arguments Exp _ _%qfT _%N.
-Arguments Equal _ _%qfT _%qfT.
-Arguments And _ _%qfT _%qfT.
-Arguments Or _ _%qfT _%qfT.
-Arguments Implies _ _%qfT _%qfT.
-Arguments Not _ _%qfT.
+Arguments Add _ _%_qfT _%_qfT.
+Arguments Opp _ _%_qfT.
+Arguments NatMul _ _%_qfT _%_N.
+Arguments Mul _ _%_qfT _%_qfT.
+Arguments Mul _ _%_qfT _%_qfT.
+Arguments Exp _ _%_qfT _%_N.
+Arguments Equal _ _%_qfT _%_qfT.
+Arguments And _ _%_qfT _%_qfT.
+Arguments Or _ _%_qfT _%_qfT.
+Arguments Implies _ _%_qfT _%_qfT.
+Arguments Not _ _%_qfT.
 
 Arguments Bool [R].
 Prenex Implicits Const Add Opp NatMul Mul Exp Bool Unit And Or Implies Not Lt.