From ef36545c3b00b3c884c921271d14d73d29398e28 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 3 Nov 2024 16:10:28 +0000 Subject: [PATCH] fully qualify unimported ZArith lemmas --- implementations/QType_rationals.v | 2 +- implementations/fast_rationals.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/implementations/QType_rationals.v b/implementations/QType_rationals.v index b992245..9392351 100644 --- a/implementations/QType_rationals.v +++ b/implementations/QType_rationals.v @@ -159,7 +159,7 @@ Qed. Next Obligation. rewrite spec_compare in *. destruct (Qcompare_spec (to_Q x) (to_Q y)); try discriminate; try intuition. - now apply Zeq_le. + now apply Zorder.Zeq_le. now apply orders.lt_le. Qed. diff --git a/implementations/fast_rationals.v b/implementations/fast_rationals.v index f735d0b..3530ce1 100644 --- a/implementations/fast_rationals.v +++ b/implementations/fast_rationals.v @@ -58,7 +58,7 @@ Proof. case_eq (BigN.eqb d BigN.zero); intros Ed2; [reflexivity |]. rewrite BigZ.spec_compare in Ed. destruct (proj2 (not_true_iff_false _) Ed2). - apply BigN.eqb_eq. symmetry. now apply Zcompare_Eq_eq. + apply BigN.eqb_eq. symmetry. now apply Zcompare.Zcompare_Eq_eq. unfold BigQ.mul. simpl. rewrite right_identity. reflexivity. destruct (BigZ.compare_spec BigZ.zero (BigZ.Pos d)); try discriminate. destruct (orders.lt_not_le_flip 0 ('d : bigZ)); trivial.