Commit 0429c257 authored by Robbert Krebbers's avatar Robbert Krebbers

Consider simpl and clearing introduction patterns as persistent.

This fixes the bug that when having:

    iDestruct (foo with "H") as "{H1 H2} #[H1 H2]"

The hypothesis H would not be kept.
parent e5c102c3
......@@ -144,6 +144,9 @@ Fixpoint intro_pat_persistent (p : intro_pat) :=
| IPureElim => true
| IAlwaysElim _ => true
| IList pps => forallb (forallb intro_pat_persistent) pps
| ISimpl => true
| IClear _ => true
| IClearFrame _ => true
| _ => false
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