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

fully qualify unimported ZArith lemmas (for coq/coq#19801)
coq-community · Nov 3, 2024 · 9db3142 · 9db3142
2 parents 5faa2f7 + ef36545
commit 9db3142
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git 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
@@ -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.