iEval (eauto) "corrupts" goal
While I ran into !269 (merged), I also ended up learning that iEval (eauto)
can "corrupt" the goal by calling iStartProof
again:
1 subgoal
Σ : gFunctors
H : heapG Σ
c1, c2 : val
A1, A2, B1, B2 : lty Σ
v1, v2 : val
w2, w1 : language.val heap_lang
============================
"HwB2" : B2 w2
"HwB1" : B1 w1
--------------------------------------∗
⌜--------------------------------------∗
(B1 * B2)%lty (w1, w2)%V
⌝
(from Blaisorblade/examples@e9851f64).
Minimized version:
From iris.base_logic.lib Require Import invariants.
From iris.proofmode Require Import tactics.
Lemma foo {Σ}: True ⊢ True : iProp Σ.
Proof.
iIntros.
iEval (info_eauto).
Show.
(*Equal to: *)
(* iEval (iStartProof; iPureIntro). *)
gives:
1 subgoal
Σ : gFunctors
a : True
============================
--------------------------------------∗
⌜?P⌝