1 files changed, 21 insertions, 0 deletions
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 25385a77a5..09f0f5ba03 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -11,6 +11,27 @@
 (** This module implements various tactics used to simplify the goals produced by Program,
    which are also generally useful. *)
 
+(** Debugging tactics to show the goal during evaluation. *)
+
+Ltac show_goal := match goal with [ |- ?T ] => idtac T end.
+
+Ltac show_hyp id := 
+  match goal with 
+    | [ H := ?b : ?T |- _ ] => 
+      match H with
+        | id => idtac id ":=" b ":" T
+      end
+    | [ H : ?T |- _ ] => 
+      match H with
+        | id => idtac id  ":"  T
+      end
+  end.
+
+Ltac show_hyps :=
+  try match reverse goal with
+        | [ H : ?T |- _ ] => show_hyp H ; fail
+      end.
+
 (** The [do] tactic but using a Coq-side nat. *)
 
 Ltac do_nat n tac :=