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
---
 plugins/subtac/subtac.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'plugins')

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 ())) ()
 
-- 
cgit v1.2.3