1 files changed, 13 insertions, 0 deletions
diff --git a/src/Util/Tactics/Revert.v b/src/Util/Tactics/Revert.v
new file mode 100644
index 000000000..5f549025d
--- /dev/null
+++ b/src/Util/Tactics/Revert.v
@@ -0,0 +1,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.