blob: 5f549025d7fe815cb50567db52247d2230477661 (
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' : appcontext[H] |- _ ] => fail
| [ |- appcontext[H] ] => fail
| _ => idtac
end;
revert H
end.
Ltac reverse_nondep := repeat revert_last_nondep.
|
