Merge pull request #87 from proux01/rocq21849

Adapt to rocq-prover/rocq#21849

Author: proux01

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.

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.