Commit 7c1a6c43 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

NEw reference for tests.

parent c83f4824
......@@ -62,3 +62,31 @@ In nested Ltac calls to "iFrame (constr)",
"<iris.proofmode.ltac_tactics.iFrame_go>" and
"<iris.proofmode.ltac_tactics.iFrameHyp>", last call failed.
Tactic failure: iFrame: cannot frame (P i).
1 subgoal
I : biIndex
Σ : gFunctors
invG0 : invG Σ
N : namespace
P : iProp Σ
============================
"H" : ⎡ inv N (<pers> P) ⎤
"H2" : ⎡ ▷ <pers> P ⎤
--------------------------------------□
|={⊤ ∖ ↑N}=> ⎡ ▷ <pers> P ⎤ ∗ (|={⊤}=> ⎡ ▷ P ⎤)
1 subgoal
I : biIndex
Σ : gFunctors
invG0 : invG Σ
N : namespace
P : iProp Σ
============================
"H" : ⎡ inv N (<pers> P) ⎤
"H2" : ⎡ ▷ <pers> P ⎤
--------------------------------------□
"Hclose" : ⎡ ▷ <pers> P ={⊤ ∖ ↑N,⊤}=∗ emp ⎤
--------------------------------------∗
|={⊤ ∖ ↑N,⊤}=> ⎡ ▷ P ⎤
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