Commit 5e608261 authored by Ralf Jung's avatar Ralf Jung

fix clear pattern in destruct pattern

parent 045c2d15
......@@ -587,6 +587,12 @@ Proof.
iIntros "?". iExists _. iApply modal_if_lemma2. done.
Qed.
Lemma test_iDestruct_clear P Q R :
P - (Q R) - True.
Proof.
iIntros "HP HQR". iDestruct "HQR" as "{HP} [HQ HR]". done.
Qed.
End tests.
(** Test specifically if certain things print correctly. *)
......
......@@ -1102,19 +1102,19 @@ Local Ltac iDestructHypGo Hz pat :=
| IModalElim ?pat => iModCore Hz; iDestructHypGo Hz pat
| _ => fail "iDestruct:" pat "invalid"
end.
Local Ltac iDestructHypFindPat H pat found pats :=
Local Ltac iDestructHypFindPat Hgo pat found pats :=
lazymatch pats with
| [] =>
lazymatch found with
| true => pm_prettify (* post-tactic prettification *)
| false => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
| ISimpl :: ?pats => simpl; iDestructHypFindPat H pat found pats
| IClear ?H :: ?pats => iClear H; iDestructHypFindPat H pat found pats
| IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat H pat found pats
| ISimpl :: ?pats => simpl; iDestructHypFindPat Hgo pat found pats
| IClear ?H :: ?pats => iClear H; iDestructHypFindPat Hgo pat found pats
| IClearFrame ?H :: ?pats => iFrame H; iDestructHypFindPat Hgo pat found pats
| ?pat :: ?pats =>
lazymatch found with
| false => iDestructHypGo H pat; iDestructHypFindPat H pat true pats
| false => iDestructHypGo Hgo pat; iDestructHypFindPat Hgo pat true pats
| true => fail "iDestruct:" pat "should contain exactly one proper introduction pattern"
end
end.
......
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