From d7609a04877b54dbf019cfd51abedacb955f1b20 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 10 Sep 2009 21:03:08 +0000
Subject: Misc fixes: - better implicits for [antisymmetry] - don't throw away
 implicit arguments info when doing [Program Definition : type.] - add
 standard debugging tactics to print goals/hyps in Program.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12317 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Tactics.v | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'theories/Program')

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 :=
-- 
cgit v1.2.3