From 768be4ca8a1ee7a9ff9c3bee0e13d7e66228895d Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 13 Feb 2018 18:04:54 +0100
Subject: [PATCH] solve AsValid without solving all the other evars first
---
theories/proofmode/tactics.v | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 4a1451dc3..ab862cc2b 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -628,8 +628,8 @@ Tactic Notation "iIntoValid" open_constr(t) :=
let e := fresh in evar (e:id T);
let e' := eval unfold e in e in clear e; go (t e')
| _ =>
- let tT' := eval cbv zeta in tT in apply (as_valid_1 tT');
- [apply _ || fail "iPoseProof: not a BI assertion"|exact t]
+ let tT' := eval cbv zeta in tT in eapply (as_valid_1 tT');
+ [solve [ typeclasses eauto with typeclass_instances ] || fail "iPoseProof: not a BI assertion"|exact t]
end in
go t.
--
GitLab