Adapt to https://github.com/coq/coq/pull/19801

theories/common.v

@@ -1,5 +1,5 @@
 From elpi Require Import elpi.
-From Coq Require Import QArith.
+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.
@@ -12,7 +12,7 @@
 
 Local Open Scope ring_scope.
 
 Implicit Types (V : nmodType) (R : semiRingType) (F : fieldType).
 
 (* Some basic facts about `Decimal.uint` and `Hexadecimal.uint`               *)
 
@@ -181,7 +181,7 @@
 
 (* Type for reified expressions                                               *)
 
 Inductive RExpr : semiRingType -> Type :=
   (* 0 *)
   | R0 R : RExpr R
   (* addition *)
@@ -192,11 +192,11 @@
   (* natmul *)
   | RMuln R : RExpr R -> RExpr nat -> RExpr R
   (* opposite and subtraction *)
   | ROpp (R : ringType) : RExpr R -> RExpr R
   | RZOpp : RExpr Z -> RExpr Z
   | RZSub : RExpr Z -> RExpr Z -> RExpr Z
   (* intmul *)
   | RMulz (R : ringType) : RExpr R -> RExpr int -> RExpr R
   (* 1 *)
   | R1 R : RExpr R
   (* multiplication *)
@@ -309,7 +309,7 @@
 
 Section norm.
 
 Variables (R' : semiRingType) (R_of_N : N -> R').
 Variables (zero : R') (add : R' -> R' -> R').
 Variables (one : R') (mul : R' -> R' -> R') (exp : R' -> N -> R').
 
@@ -385,7 +385,7 @@
 
 Section correct.
 
 Variables (R' : semiRingType).
 
 Notation Rnorm :=
   (Rnorm (fun n => (nat_of_N n)%:R) 0 +%R 1 *%R (fun x n => x ^+ N.to_nat n)).
@@ -448,7 +448,7 @@
 
 Section norm.
 
 Variables (R' : ringType) (R_of_Z : Z -> R').
 Variables (zero : R') (add : R' -> R' -> R').
 Variables (opp : R' -> R') (sub : R' -> R' -> R').
 Variables (one : R') (mul : R' -> R' -> R') (exp : R' -> N -> R').
@@ -555,7 +555,7 @@
 
 Section correct.
 
 Variables (R' : ringType).
 
 Notation Rnorm :=
   (Rnorm (fun n : Z => (int_of_Z n)%:~R) 0 +%R -%R (fun x y => x - y)
@@ -650,7 +650,7 @@
 
 Section norm.
 
 Variables (F : ringType) (F_of_Z : Z -> F).
 Variables (zero : F) (add : F -> F -> F) (opp : F -> F) (sub : F -> F -> F).
 Variables (one : F) (mul : F -> F -> F) (exp : F -> N -> F) (inv : F -> F).
 
@@ -857,7 +857,7 @@
 
 Section norm.
 
 Variables (F : ringType) (F_of_Z : bool -> Z -> F).
 Variables (zero : F) (add : F -> F -> F) (opp : F -> F) (sub : F -> F -> F).
 Variables (one : F) (mul : F -> F -> F) (exp : F -> N -> F) (inv : F -> F).
 

theories/lra.v

@@ -1,8 +1,8 @@
 From elpi Require Import elpi.
-From Coq Require Import QArith Ring.
+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.
 From mathcomp.zify Require Import ssrZ zify.
 From mathcomp.algebra_tactics Require Import common.
 From mathcomp.algebra_tactics Extra Dependency "common.elpi" as common.
@@ -394,7 +394,7 @@
 Elpi Tactic lra.
 Elpi Accumulate Db canonicals.db.
 Elpi Accumulate File common lra.
 Elpi Typecheck.
 
 Tactic Notation "lra" := elpi lra "lra_witness" "tacF" "tacR" 0.
 Tactic Notation "nra" := elpi lra "nra_witness" "tacF" "tacR" 0.