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

3 files changed, 26 insertions, 3 deletions

diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index ed8ecfac4f..8b1d20e6de 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -75,11 +75,13 @@ let start_proof_com env isevars sopt kind (bl,t) hook =
 	next_global_ident_away false (id_of_string "Unnamed_thm")
  	  (Pfedit.get_all_proof_names ())
   in
-  let evm, c, typ, _imps = 
+  let evm, c, typ, imps = 
     Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None 
   in
   let c = solve_tccs_in_type env id isevars evm c typ in
-    Command.start_proof id kind c hook	
+    Command.start_proof id kind c (fun loc gr -> 
+      Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true imps;
+      hook loc gr)
       
 let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) ()
 
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index 4f69b52c28..edfd1094d9 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -179,7 +179,7 @@ Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
 (** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
 
 Class Antisymmetric A eqA `{equ : Equivalence A eqA} (R : relation A) :=
-  antisymmetry : forall x y, R x y -> R y x -> eqA x y.
+  antisymmetry : forall {x y}, R x y -> R y x -> eqA x y.
 
 Program Definition flip_antiSymmetric `(Antisymmetric A eqA R) :
   Antisymmetric A eqA (flip R).
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 :=