Commit 623c2839 authored by Robbert Krebbers's avatar Robbert Krebbers

Fix bug: iIntros "%" was doing the wrong thing.

parent 427a99c4
Pipeline #448 passed with stage
......@@ -681,7 +681,7 @@ Tactic Notation "iIntros" constr(pat) :=
| IName ?H :: ?pats => iIntro H; go pats
| IPersistent IAnom :: ?pats => let H := iFresh in iIntro #H; go pats
| IAnom :: ?pats => let H := iFresh in iIntro H; go pats
| IAnomPure :: ?pats => iPureIntro; go pats
| IAnomPure :: ?pats => iIntro {?}; go pats
| IPersistent ?pat :: ?pats =>
let H := iFresh in iIntro #H; iDestructHyp H as pat; go pats
| ?pat :: ?pats =>
......
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