Commit bfdd67a7 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix `iIntros` regression caused by b0ae1102.

parent c95907b9
......@@ -939,7 +939,7 @@ Tactic Notation "iIntros" constr(pat) :=
| ?pat :: ?pats =>
let H := iFresh in iIntro H; iDestructHyp H as pat; go pats
end
in let pats := intro_pat.parse pat in iStartProof; go pats.
in let pats := intro_pat.parse pat in try iStartProof; go pats.
Tactic Notation "iIntros" := iIntros [IAll].
Tactic Notation "iIntros" "(" simple_intropattern(x1) ")" :=
......
......@@ -93,6 +93,10 @@ Proof.
iIntros "# _ //".
Qed.
Lemma test_very_fast_iIntros P :
x y : nat, x = y - P - P.
Proof. by iIntros. Qed.
Lemma test_iDestruct_spatial_and P Q1 Q2 : P (Q1 Q2) - P Q1.
Proof. iIntros "[H1 [H2 _]]". by iFrame. Qed.
......
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