diff options
| author | sacerdot | 2005-05-20 16:14:52 +0000 |
|---|---|---|
| committer | sacerdot | 2005-05-20 16:14:52 +0000 |
| commit | d361ee5b960e1a54d451dc81557f19e504baa42a (patch) | |
| tree | 417cf2b9bce2dcaf293cc9ab11ad5ebede7d2dc9 /tactics | |
| parent | d0a324eef4d35a87e300a2b660b26fdbe2043d92 (diff) | |
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
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 11 | ||||
| -rw-r--r-- | tactics/tacinterp.mli | 3 |
2 files changed, 14 insertions, 0 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 1a9ae4b0fd..8194a4cf7e 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 diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 83b0d7acd9..56f2a3e40a 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -140,3 +140,6 @@ val overwriting_interp_add : string * (interp_sign -> Coqast.t -> value) -> val declare_xml_printer : (out_channel -> Environ.env -> Evd.evar_map -> constr -> unit) -> unit + +(* printing *) +val print_ltac : Libnames.qualid -> std_ppcmds |