Commit 4c38ac07 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Let iRevertIntros ensure that we are in the proofmode.

This fixes issue #61.
parent af80361b
......@@ -861,7 +861,7 @@ Tactic Notation "iRevertIntros" constr(Hs) "with" tactic(tac) :=
match p with true => constr:([IAlwaysElim (IName H)]) | false => H end in
iIntros H'
end in
iElaborateSelPat Hs go.
try iStartProof; iElaborateSelPat Hs go.
Tactic Notation "iRevertIntros" "(" ident(x1) ")" constr(Hs) "with" tactic(tac):=
iRevertIntros Hs with (iRevert (x1); tac; iIntros (x1)).
Supports Markdown
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