From 72a2b8d5cde37240d35e19ac128c4763039a4432 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 20 Nov 2018 15:32:35 +0100
Subject: [PATCH] One more occurence...
---
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 b5602fbec..763137c05 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -628,7 +628,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
|first
--
GitLab