Commit 9a93c850 authored by Robbert Krebbers's avatar Robbert Krebbers

Factor out anonymous rec in `iRevertIntros` to get cleaner Ltac backtraces.

parent b0c4d25c
......@@ -1747,14 +1747,15 @@ Tactic Notation "iIntros" constr(p) "(" simple_intropattern(x1)
iIntros p; iIntros ( x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x15 ); iIntros p2.
(* Used for generalization in iInduction and iLöb *)
Tactic Notation "iRevertIntros" constr(Hs) "with" tactic3(tac) :=
let rec go Hs :=
Ltac iRevertIntros_go Hs tac :=
lazymatch Hs with
| [] => tac
| ESelPure :: ?Hs => fail "iRevertIntros: % not supported"
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; go Hs; iIntro H as p
end in
try iStartProof; let Hs := iElaborateSelPat Hs in go Hs.
| ESelIdent ?p ?H :: ?Hs => iRevertHyp H; iRevertIntros_go Hs tac; iIntro H as p
Tactic Notation "iRevertIntros" constr(Hs) "with" tactic3(tac) :=
try iStartProof; let Hs := iElaborateSelPat Hs in iRevertIntros_go Hs tac.
Tactic Notation "iRevertIntros" "(" ident(x1) ")" constr(Hs) "with" tactic3(tac):=
iRevertIntros Hs with (iRevert (x1); tac; iIntros (x1)).
Markdown is supported
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment