Merge pull request #107 from proux01/coq_19801

Adapt to coq/coq#19801
math-comp · Jan 17, 2025 · 9139306 · 9139306
2 parents 12e9b64 + f221d60
commit 9139306
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/theories/common.v b/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.

diff --git a/theories/lra.v b/theories/lra.v
@@ -1,5 +1,5 @@
 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.