ajout Show Intro(s)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1825 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 39 insertions, 0 deletions

diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4
index 24f3a00c9a..ae1c925996 100644
--- a/parsing/g_proofs.ml4
+++ b/parsing/g_proofs.ml4
@@ -71,6 +71,8 @@ GEXTEND Gram
       | IDENT "Focus"; n = numarg -> <:ast< (FOCUS $n) >>
       | IDENT "Unfocus" -> <:ast< (UNFOCUS) >>
       | IDENT "Show" -> <:ast< (SHOW) >>
+      | IDENT "Show"; IDENT "Intro" -> <:ast< (SHOWINTRO) >>
+      | IDENT "Show"; IDENT "Intros" -> <:ast< (SHOWINTROS) >>
       | IDENT "Show"; IDENT "Implicits" -> <:ast< (SHOWIMPL) >>
       | IDENT "Show"; IDENT "Node" -> <:ast< (ShowNode) >>
       | IDENT "Show"; IDENT "Script" -> <:ast< (ShowScript) >>
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6f315f358b..e57eb11b65 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -59,6 +59,7 @@ val dyn_mutual_cofix : tactic_arg list -> tactic
 (*s Introduction tactics. *)
 
 val next_global_ident_away : identifier -> identifier list -> identifier
+val fresh_id : identifier list -> identifier -> goal sigma -> identifier
 
 val intro                : tactic
 val introf               : tactic
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 2a840558f2..d36779b43d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1770,3 +1770,39 @@ let _ = vinterp_add "DumpUniverses"
 		 )
 	     | _ -> 
 		 anomaly "DumpUniverses : expects a filename or nothing as argument") 
+
+(* Simulate the Intro(s) tactic *)
+
+open Tactics
+
+let id_of_name = function
+    Anonymous -> id_of_string "H"
+  | Name id   -> id;;
+
+let rec do_renum avoid gl = function
+    [] -> ""
+  | [n] -> (string_of_id (fresh_id avoid (id_of_name n) gl))
+  | n :: l -> let id = fresh_id avoid (id_of_name n) gl in
+        (string_of_id id)^" "^(do_renum (id :: avoid) gl l)
+
+let _ = vinterp_add "SHOWINTRO" 
+	  (function 
+	     | [] -> 
+		 (fun () ->
+		    let pf = get_pftreestate() in
+		    let gl = nth_goal_of_pftreestate 1 pf in
+		    let l,_= decompose_prod (strip_outer_cast (pf_concl gl)) in
+		    let n = List.hd (List.rev_map fst l) in
+		      message (string_of_id (fresh_id [] (id_of_name n) gl)))
+	     | _ -> bad_vernac_args "Show Intro")
+
+let _ =  vinterp_add "SHOWINTROS"
+	   (function 
+	      | [] -> 
+		  (fun () ->
+		     let pf = get_pftreestate() in
+		     let gl = nth_goal_of_pftreestate 1 pf in
+		     let l,_= decompose_prod (strip_outer_cast (pf_concl gl)) in
+		     let l = List.rev_map fst l in
+		       message (do_renum [] gl l))
+	      | _ -> bad_vernac_args "Show Intros")