Merge pull request #78 from JasonGross/fix-for-more-rapply-10760

Fix for a new rapply tactic
coq-community · Oct 16, 2023 · 83822de · 83822de
2 parents fbb6ebe + 975c458
commit 83822de
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 9 deletions.
diff --git a/implementations/nonneg_semiring_elements.v b/implementations/nonneg_semiring_elements.v
@@ -62,7 +62,7 @@ Proof. split. trivial. apply _. Qed.
 
 (* Misc *)
 Global Instance NonNeg_trivial_apart `{!TrivialApart R} :  TrivialApart (R⁺).
-Proof. intros x y. now rapply trivial_apart. Qed.
+Proof. intros x y. now Tactics.rapply trivial_apart. Qed.
 
 Global Instance NonNeg_equiv_dec `{∀ x y : R, Decision (x = y)} : ∀ x y: R⁺, Decision (x = y)
   := λ x y, decide_rel (=) ('x : R) ('y : R).

diff --git a/implementations/semiring_pairs.v b/implementations/semiring_pairs.v
@@ -17,7 +17,7 @@ Global Instance SRpair_equiv : Equiv (SRpair SR) | 4 := λ x y, pos x + neg y =
 Global Instance SRpair_apart `{Apart SR} : Apart (SRpair SR) := λ x y, pos x + neg y ≶ pos y + neg x.
 
 Global Instance SRpair_trivial_apart `{!TrivialApart SR} :  TrivialApart (SRpair SR).
-Proof. intros x y. now rapply trivial_apart. Qed.
+Proof. intros x y. now Tactics.rapply trivial_apart. Qed.
 
 Instance: Setoid (SRpair SR).
 Proof.
@@ -256,7 +256,7 @@ Section with_full_pseudo_semiring_order.
      setoid_replace (zp + yn + xn) with (zp + xn + yn) by ring.
      setoid_replace (yp + zn + xn) with (zn + (yp + xn)) by ring.
      eassumption.
-    intros [??] [??]. now rapply tight_apart.
+    intros [??] [??]. now Tactics.rapply tight_apart.
   Qed.
 
   Instance: FullPseudoOrder SRpair_le SRpair_lt.
@@ -273,8 +273,8 @@ Section with_full_pseudo_semiring_order.
       setoid_replace (zp + yn + xn) with (zp + xn + yn) by ring.
       setoid_replace (yp + zn + xn) with (zn + (yp + xn)) by ring.
       eassumption.
-     intros [??] [??]. now rapply apart_iff_total_lt.
-    intros [??] [??]. now rapply le_iff_not_lt_flip.
+     intros [??] [??]. now Tactics.rapply apart_iff_total_lt.
+    intros [??] [??]. now Tactics.rapply le_iff_not_lt_flip.
   Qed.
 
   Instance: ∀ z : SRpair SR, StrongSetoid_Morphism (z *.).

diff --git a/theory/ring_congruence.v b/theory/ring_congruence.v
@@ -50,16 +50,16 @@ Section quotient_ring.
   Qed.
 
   Instance: Proper ((=) ==> (=) ==> (=)) quotient_plus.
-  Proof. intros [?] [?] E1 [?] [?] E2. now rapply ring_congr_plus. Qed.
+  Proof. intros [?] [?] E1 [?] [?] E2. now Tactics.rapply ring_congr_plus. Qed.
 
   Instance: Proper ((=) ==> (=) ==> (=)) quotient_mult.
-  Proof. intros [?] [?] E1 [?] [?] E2. now rapply ring_congr_mult. Qed.
+  Proof. intros [?] [?] E1 [?] [?] E2. now Tactics.rapply ring_congr_mult. Qed.
 
   Instance: Proper ((=) ==> (=)) quotient_negate.
-  Proof. intros [?] [?] E. now rapply ring_congr_negate. Qed.
+  Proof. intros [?] [?] E. now Tactics.rapply ring_congr_negate. Qed.
 
   Global Instance: Setoid_Morphism quotient_inject.
-  Proof. split; try apply _. intros ?? E. now rapply ring_congr_subrelation. Qed.
+  Proof. split; try apply _. intros ?? E. now Tactics.rapply ring_congr_subrelation. Qed.
 
   Global Instance: Ring (Quotient A R).
   Proof.