New command: "Print Ltac qualid" to print user defined tactics.

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

1 files changed, 11 insertions, 0 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1a9ae4b0f..8194a4cf7 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2175,6 +2175,17 @@ let (inMD,outMD) =
      classify_function = (fun (_,o) -> Substitute o);       
      export_function = (fun x -> Some x)}
 
+let print_ltac id =
+ try
+  let kn = Nametab.locate_tactic id in
+  let t = lookup kn in
+   str "Ltac" ++ spc() ++ pr_qualid id ++ str ":=" ++ spc() ++
+    Pptacticnew.pr_glob_tactic (Global.env ()) t
+ with
+  Not_found ->
+   errorlabstrm "print_ltac"
+    (pr_qualid id ++ spc() ++ str "is not a user defined tactic")
+
 (* Adds a definition for tactics in the table *)
 let make_absolute_name (loc,id) =
   let kn = Lib.make_kn id in