diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/g_ltac.ml4 | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/tactics/g_ltac.ml4 b/tactics/g_ltac.ml4 index 3573ca717..5c0ae215d 100644 --- a/tactics/g_ltac.ml4 +++ b/tactics/g_ltac.ml4 @@ -404,3 +404,8 @@ VERNAC COMMAND EXTEND VernacTacticNotation CLASSIFIED AS SIDEFF Metasyntax.add_tactic_notation (Locality.make_module_locality l, n, r, e) ] END + +VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY +| [ "Print" "Ltac" reference(r) ] -> + [ msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ] +END |