blob: 78c94f956ec45123d730047b2d54f96f78d08964 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
(** Like [Coq.Program.Tactics.revert_last], but only for non-dependent hypotheses *)
Ltac revert_last_nondep :=
match goal with
| [ H : _ |- _ ]
=> lazymatch goal with
| [ H' : context[H] |- _ ] => fail
| [ |- context[H] ] => fail
| _ => idtac
end;
revert H
end.
Ltac reverse_nondep := repeat revert_last_nondep.
|
