1 files changed, 14 insertions, 0 deletions
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index 5ff9d203c..aa8093308 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -308,3 +308,17 @@ Ltac tac_on_subterms tac :=
          | [ |- context[?t] ]
            => progress tac t
          end.
+
+(** 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.