From 394075ccaa09678d9707afd1e533d136f9747375 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Nov 2018 15:30:43 +0100
Subject: [PATCH] Do not manually apply TC instances using `refine`.
After Coq PR #7825 this will create unwanted evars.
---
theories/proofmode/ltac_tactics.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/proofmode/ltac_tactics.v b/theories/proofmode/ltac_tactics.v
index c4594b699..b5602fbec 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -601,7 +601,7 @@ Ltac iSpecializePat_go H1 pats :=
fail "iSpecialize:" H1 "not found"
|solve_to_wand H1
|lazymatch m with
- | GSpatial => notypeclasses refine (add_modal_id _ _)
+ | GSpatial => class_apply add_modal_id
| GModal => iSolveTC || fail "iSpecialize: goal not a modality"
end
|pm_reflexivity ||
--
GitLab