From 2abfa29636a8fdc184859d5445118df8d469df3b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 14 Feb 2018 10:06:24 +0100
Subject: [PATCH] explain why we use typeclasses eauto
---
theories/proofmode/tactics.v | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index ab862cc2b..c3be4ca67 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -629,6 +629,11 @@ Tactic Notation "iIntoValid" open_constr(t) :=
let e' := eval unfold e in e in clear e; go (t e')
| _ =>
let tT' := eval cbv zeta in tT in eapply (as_valid_1 tT');
+ (* Doing [apply _] here fails because that will try to solve all evars
+ whose type is a typeclass, in dependency order (according to Matthieu).
+ If one fails, it aborts. However, we rely on progress on the main goal
+ ([AsValid ...]) to unify some of these evars and hence enable progress
+ elsewhere. With [typeclasses eauto], that seems to work better. *)
[solve [ typeclasses eauto with typeclass_instances ] || fail "iPoseProof: not a BI assertion"|exact t]
end in
go t.
--
GitLab