Add Tactics.PrintContext

1 files changed, 12 insertions, 0 deletions

diff --git a/src/Util/Tactics/PrintContext.v b/src/Util/Tactics/PrintContext.v
new file mode 100644
index 000000000..1a774bdfc
--- /dev/null
+++ b/src/Util/Tactics/PrintContext.v
@@ -0,0 +1,12 @@
+Ltac print_context _ :=
+  lazymatch goal with
+  | [ H : ?T |- False ]
+    => try ((clear H || fail 10000 "Anomaly in print_context: could not clear" H); print_context (); fail);
+       match goal with
+       | _ => let body := (eval cbv delta [H] in H) in
+              idtac H ":=" body ":" T
+       | _ => idtac H ":" T
+       end
+  | [ |- False ] => idtac
+  | [ |- _ ] => try (exfalso; print_context (); fail)
+  end.