Adapt to https://github.com/math-comp/math-comp/pull/1448

theories/common.v

@@ -1,7 +1,8 @@
+From mathcomp Require all_algebra. (* Remove this line when requiring Rocq > 9.1 *)
 From elpi Require Import elpi.
 From Coq Require Import PeanoNat BinNat Zbool QArith.
 From Coq.micromega Require Import OrderedRing RingMicromega.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint.
 From mathcomp.zify Require Import ssrZ zify.
 
 Import Order.TTheory GRing.Theory Num.Theory.
@@ -1331,7 +1332,7 @@
 Proof.
 rewrite /Qeq_bool /R_of_Q /= eqr_div ?pnatr_eq0; try lia.
 rewrite !pmulrn -!intrM eqr_int -!/(int_of_Z (Z.pos _)) -!rmorphM /=.
 by rewrite (can_eq int_of_ZK); apply/idP/eqP => /Zeq_is_eq_bool.
 Qed.
 
 Lemma R_of_Q_le x y : Qle_bool x y = (R_of_Q x <= R_of_Q y :> F).

theories/lra.v

@@ -1,5 +1,6 @@
+From mathcomp Require all_algebra. (* Remove this line when requiring Rocq > 9.1 *)
 From elpi Require Import elpi.
 From Coq Require Import BinNat QArith Ring.
 From Coq.micromega Require Import RingMicromega QMicromega EnvRing Tauto Lqa.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
 From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint.
@@ -63,10 +64,10 @@
   | OpGt  => fun x y => lt y x
   end.
 
-Definition Reval_op2 k : Op2 -> R -> R -> rtyp k :=
+Definition Reval_op2 k : Op2 -> R -> R -> eKind k :=
   match k with isProp => Reval_pop2 | isBool => Reval_bop2 end.
 
-Definition Reval_formula k (ff : RFormula R) : rtyp k :=
+Definition Reval_formula k (ff : RFormula R) : eKind k :=
   let (lhs,o,rhs) := ff in Reval_op2 k o (Reval lhs) (Reval rhs).
 
 Definition Rnorm_formula k (ff : RFormula R) :=
@@ -93,8 +94,8 @@
 - by move=> ff1 IH1 ff2 IH2; congr eq.
 Qed.
 
-Definition Reval_PFormula (e : PolEnv R) k (ff : Formula Z) : rtyp k :=
-  let eval := PEeval add mul sub opp R_of_Z id exp e in
+Definition Reval_PFormula (e : PolEnv R) k (ff : Formula Z) : eKind k :=
+  let eval := EnvRing.PEeval add mul sub opp R_of_Z id exp e in
   let (lhs,o,rhs) := ff in Reval_op2 k o (eval lhs) (eval rhs).
 
 Lemma pop2_bop2 (op : Op2) (q1 q2 : R) :
@@ -104,7 +105,9 @@
 Lemma Reval_formula_compat (env : PolEnv R) k (f : Formula Z) :
   hold k (Reval_PFormula env k f) <->
   eval_formula add mul sub opp eqProp le lt R_of_Z id exp env f.
-Proof. by case: f => lhs op rhs; case: k => //=; rewrite pop2_bop2. Qed.
+Proof.
+by case: f => lhs op rhs; case: k => /=; rewrite ?pop2_bop2; case: op.
+Qed.
 
 End Rnorm_formula.
 
@@ -117,7 +120,7 @@
 
 Definition ZTautoChecker (f : BFormula (Formula Z) isProp) (w: list (Psatz Z)) :
     bool :=
-  @tauto_checker
+  @Tauto.tauto_checker
     (Formula Z) (NFormula Z) unit
     (check_inconsistent 0 Z.eqb Z.leb)
     (nformula_plus_nformula 0 Z.add Z.eqb)
@@ -208,7 +211,7 @@
 - by move=> ff1 IH1 ff2 IH2; congr eq.
 Qed.
 
-Definition Feval_PFormula (e : PolEnv F) k (ff : Formula Q) : rtyp k :=
+Definition Feval_PFormula (e : PolEnv F) k (ff : Formula Q) : eKind k :=
   let eval := eval_pexpr add mul sub opp F_of_Q id exp e in
   let (lhs,o,rhs) := ff in Feval_op2 k o (eval lhs) (eval rhs).
 
@@ -219,7 +222,9 @@
 Lemma Feval_formula_compat env b f :
   hold b (Feval_PFormula env b f) <->
   eval_formula add mul sub opp eqProp le lt F_of_Q id exp env f.
-Proof. by case: f => lhs op rhs; case: b => //=; rewrite pop2_bop2'. Qed.
+Proof.
+by case: f => lhs op rhs; case: b => /=; rewrite ?pop2_bop2'; case: op.
+Qed.
 
 End Fnorm_formula.
 

theories/ring.v

@@ -1,5 +1,6 @@
+From mathcomp Require all_algebra. (* Remove this line when requiring Rocq > 9.1 *)
 From elpi Require Import elpi.
 From Coq Require Import ZArith Ring Ring_polynom Field_theory.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat choice seq.
 From mathcomp Require Import fintype finfun bigop order ssralg ssrnum ssrint.
 From mathcomp.zify Require Import ssrZ zify.