Commit 3b961083 authored by Robbert Krebbers's avatar Robbert Krebbers

Simplify implementation of `iRevertIntros`.

parent ff007045
......@@ -1464,9 +1464,10 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs =>
iRevert H; go Hs;
let H' :=
match p with true => constr:([IAlwaysElim (IIdent H)]) | false => H end in
iIntros H'
match p with
| true => iIntro #H
| false => iIntro H
end in
try iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
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