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

1 files changed, 21 insertions, 0 deletions

diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 25385a77a..09f0f5ba0 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 :=