Commit 768be4ca authored by Ralf Jung's avatar Ralf Jung

solve AsValid without solving all the other evars first

parent 5e1597b7
......@@ -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.
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment