From df4beedfd1f2562362c003e90e59c4d3927ba548 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 25 Jun 2018 10:18:36 +0200
Subject: [PATCH] always use notypeclasses refine
---
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 f5eea3e90..81d0a3e5e 100644
--- a/theories/proofmode/ltac_tactics.v
+++ b/theories/proofmode/ltac_tactics.v
@@ -680,7 +680,7 @@ Tactic Notation "iSpecializeCore" open_constr(H)
fail "iSpecialize:" H "not found"
|iSpecializePat H pat;
[..
- |refine (tac_specialize_persistent_helper_done _ H _ _ _);
+ |notypeclasses refine (tac_specialize_persistent_helper_done _ H _ _ _);
pm_reflexivity]
|iSolveTC ||
let Q := match goal with |- IntoPersistent _ ?Q _ => Q end in
--
GitLab