From b08fd062bb8460b807d8faa1b376e0961944c2cd Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Sun, 3 Nov 2024 16:01:41 +0000
Subject: [PATCH] adapt to coq/coq#19801 (deprecation of ZArith_base, Zeq_bool)

---
 BigQ/QMake.v | 4 +++-
 BigZ/BigZ.v  | 2 +-
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/BigQ/QMake.v b/BigQ/QMake.v
index cb8cfcb..b1561cf 100644
--- a/BigQ/QMake.v
+++ b/BigQ/QMake.v
@@ -181,7 +181,9 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
 
  Theorem spec_eq_bool: forall x y, eq_bool x y = Qeq_bool [x] [y].
  Proof.
- intros. unfold eq_bool. rewrite spec_compare. reflexivity.
+   unfold eq_bool; intros.
+   apply eq_true_iff_eq; rewrite Qeq_bool_iff, spec_compare, Qeq_alt.
+   case Qcompare; intuition congruence.
  Qed.
 
  (** [check_int] : is a reduced fraction [n/d] in fact a integer ? *)
diff --git a/BigZ/BigZ.v b/BigZ/BigZ.v
index 0582395..6548e3b 100644
--- a/BigZ/BigZ.v
+++ b/BigZ/BigZ.v
@@ -10,7 +10,7 @@
 
 Require Export BigN.
 Require Import ZProperties ZDivFloor ZSig ZSigZAxioms ZMake Ring Lia.
-Import Zpow_def Zdiv.
+Import BinNat Zpow_def Zdiv.
 
 (** * [BigZ] : arbitrary large efficient integers.