adapt to coq/coq#19801 (deprecation of ZArith_base, Zeq_bool)

coq-community · Nov 3, 2024 · b08fd06 · b08fd06
1 parent 1f014ff
commit b08fd06
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
@@ -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.