Merge pull request #94 from andres-erbsen/less-ZArith_base

adapt to coq/coq#19801 (replacing ZArith_base, Zeq_bool)
coq-community · Jan 7, 2025 · cc2d9ee · cc2d9ee
2 parents 97da402 + 0b1a1b2
commit cc2d9ee
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 2 deletions.
diff --git 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
@@ -11,7 +11,7 @@
 From Stdlib Require Import ZProperties ZDivFloor Ring Lia.
 Require Export BigN.
 Require Import ZSig ZSigZAxioms ZMake.
-Import Zpow_def Zdiv.
+Import BinNat Zpow_def Zdiv.
 
 (** * [BigZ] : arbitrary large efficient integers.