From ec161a20a983a95ef1b06406cf218f77ac9a3375 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 6 Jun 2019 14:46:28 +0200
Subject: [PATCH] Fix issue w.r.t. overly eager TC resolution introduced in
!254.
---
theories/proofmode/ltac_tactics.v | 11 ++++++-----
1 file changed, 6 insertions(+), 5 deletions(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index 755952256..b349b8914 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -740,10 +740,11 @@ Tactic Notation "iPoseProofCoreLem"
try iSolveTC.
(** There is some hacky stuff going on here: because of Coq bug #6583, unresolved
-type classes in the arguments `xs` are resolved at arbitrary moments. Tactics
-like `apply`, `split` and `eexists` wrongly trigger type class search to resolve
-these holes. To avoid TC being triggered too eagerly, this tactic uses `refine`
-at most places instead of `apply`. *)
+type classes in e.g. the arguments [xs] of [iSpecializeArgs_go] are resolved at
+arbitrary moments. That is because tactics like [apply], [split] and [eexists]
+wrongly trigger type class search. To avoid TC being triggered too eagerly, the
+tactics below use [notypeclasses refine] instead of [apply], [split] and
+[eexists]. *)
Local Ltac iSpecializeArgs_go H xs :=
lazymatch xs with
| hnil => idtac
@@ -866,7 +867,7 @@ Ltac iSpecializePat_go H1 pats :=
let Hs' := iMissingHyps Hs' in
fail "iSpecialize: hypotheses" Hs' "not found"
| _ =>
- split;
+ notypeclasses refine (conj _ _);
[iFrame Hs_frame; solve_done d (*goal*)
|iSpecializePat_go H1 pats]
end]
--
GitLab