From 975c4581412e593f68f47180bd63209bb26a5b20 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 17 Sep 2019 17:03:06 -0400 Subject: [PATCH] Fix for a new rapply tactic This backwards compatible change makes math-classes work with coq/coq#10760 by replacing all instances of `rapply` which were relying on typeclass resolution happening *before* `refine` (instead of simultaneously with it) to instead invoke `Tactics.rapply` (which is the same tactic in Coq <= 8.10, and which will be the tactic rather than the `uconstr`-taking tactic notation in Coq >= 8.11). See also https://github.com/coq/coq/pull/10760#issuecomment-532399518 --- implementations/nonneg_semiring_elements.v | 2 +- implementations/semiring_pairs.v | 8 ++++---- theory/ring_congruence.v | 8 ++++---- 3 files changed, 9 insertions(+), 9 deletions(-) diff --git a/implementations/nonneg_semiring_elements.v b/implementations/nonneg_semiring_elements.v index 7fd6430e..30c1dc19 100644 --- 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 index 43e79072..582f6d4b 100644 --- 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 index d3a5f013..e01bb1f8 100644 --- a/theory/ring_congruence.v +++ b/theory/ring_congruence.v @@ -48,16 +48,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.