diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 02:09:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-20 02:20:12 +0100 |
| commit | 01cd0dd64e4faa52b5094a99e2c31ecc4e7b767d (patch) | |
| tree | 9b2ec8d20d27bf1444771aa026b57b67c0580c6e /tactics | |
| parent | 0af598b77a6242d796c66884477a046448ef1e21 (diff) | |
Moving Print Ltac to an EXTEND based command.
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 |