Added command "Locate Ltac qid".

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

7 files changed, 21 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 3212a4d42..9c56adc3d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -80,6 +80,7 @@ Tactic definitions
 
 - Ltac definitions support Local option for non-export outside modules.
 - Support for parsing non-empty lists with separators in tactic notations.
+- New command "Locate Ltac" to get the full name of an Ltac definition.
 
 Notations
 
diff --git a/library/nametab.ml b/library/nametab.ml
index 0172048af..3fa22aae3 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -470,6 +470,8 @@ let path_of_syndef kn =
 let dirpath_of_module mp =
   MPmap.find mp !the_modrevtab
 
+let path_of_tactic kn =
+  KNmap.find kn !the_tacticrevtab
 
 (* Shortest qualid functions **********************************************)
 
diff --git a/library/nametab.mli b/library/nametab.mli
index aaef53e4a..2f81ff50e 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -143,6 +143,7 @@ val full_name_module : qualid -> dir_path
 val path_of_syndef : syndef_name -> full_path
 val path_of_global : global_reference -> full_path
 val dirpath_of_module : module_path -> dir_path
+val path_of_tactic : ltac_constant -> full_path
 
 (** Returns in particular the dirpath or the basename of the full path
    associated to global reference *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index cbeb7a01e..a422bed8e 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -775,7 +775,8 @@ GEXTEND Gram
     [ [ qid = smart_global -> LocateTerm qid
       | IDENT "File"; f = ne_string -> LocateFile f
       | IDENT "Library"; qid = global -> LocateLibrary qid
-      | IDENT "Module"; qid = global -> LocateModule qid ] ]
+      | IDENT "Module"; qid = global -> LocateModule qid
+      | IDENT "Ltac"; qid = global -> LocateTactic qid ] ]
   ;
   option_value:
     [ [ n  = integer   -> IntValue n
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 5d21d26d8..dacc2b9b2 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -51,7 +51,7 @@ let pr_lname = function
 
 let pr_smart_global = pr_or_by_notation pr_reference
 
-let pr_ltac_id = Libnames.pr_reference
+let pr_ltac_ref = Libnames.pr_reference
 
 let pr_module = Libnames.pr_reference
 
@@ -814,7 +814,7 @@ let rec pr_vernac = function
           match body with
 	    | Tacexpr.TacFun (idl,b) -> idl,b
             | _ -> [], body in
-        pr_ltac_id id ++
+        pr_ltac_ref id ++
 	prlist (function None -> str " _"
                        | Some id -> spc () ++ pr_id id) idl
 	++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++
@@ -911,7 +911,7 @@ let rec pr_vernac = function
 	| PrintClasses -> str"Print Classes"
 	| PrintTypeClasses -> str"Print TypeClasses"
 	| PrintInstances qid -> str"Print Instances" ++ spc () ++ pr_smart_global qid
-	| PrintLtac qid -> str"Print Ltac" ++ spc() ++ pr_reference qid
+	| PrintLtac qid -> str"Print Ltac" ++ spc() ++ pr_ltac_ref qid
 	| PrintCoercions -> str"Print Coercions"
 	| PrintCoercionPaths (s,t) -> str"Print Coercion Paths" ++ spc() ++ pr_class_rawexpr s ++ spc() ++ pr_class_rawexpr t
 	| PrintCanonicalConversions -> str"Print Canonical Structures"
@@ -943,6 +943,7 @@ let rec pr_vernac = function
 	| LocateFile f -> str"File" ++ spc() ++ qs f
 	| LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid
 	| LocateModule qid -> str"Module" ++ spc () ++ pr_module qid
+	| LocateTactic qid -> str"Ltac" ++ spc () ++ pr_ltac_ref qid
       in str"Locate" ++ spc() ++ pr_locate loc
   | VernacComments l ->
       hov 2
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b6cf215ec..0ed1186a0 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -254,6 +254,15 @@ let print_located_module r =
 	str "No module is referred to by name ") ++ pr_qualid qid
   in msgnl msg
 
+let print_located_tactic r =
+  let (loc,qid) = qualid_of_reference r in
+  msgnl
+    (try
+      str "Ltac " ++
+      pr_path (Nametab.path_of_tactic (Nametab.locate_tactic qid))
+     with Not_found ->
+	str "No Ltac definition is referred to by " ++ pr_qualid qid)
+
 let smart_global r =
   let gr = Smartlocate.smart_global r in
     Dumpglob.add_glob (Genarg.loc_of_or_by_notation loc_of_reference r) gr;
@@ -1145,6 +1154,7 @@ let vernac_locate = function
           (Constrextern.without_symbols pr_lrawconstr) ntn sc)
   | LocateLibrary qid -> print_located_library qid
   | LocateModule qid -> print_located_module qid
+  | LocateTactic qid -> print_located_tactic qid
   | LocateFile f -> locate_file f
 
 (********************)
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index ebdec85ee..bb35445ce 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -78,6 +78,7 @@ type locatable =
   | LocateTerm of reference or_by_notation
   | LocateLibrary of reference
   | LocateModule of reference
+  | LocateTactic of reference
   | LocateFile of string
 
 type goable =