diff options
| author | Pierre-Marie Pédrot | 2016-03-20 02:09:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 02:20:12 +0100 |
| commit | 01cd0dd64e4faa52b5094a99e2c31ecc4e7b767d (patch) | |
| tree | 9b2ec8d20d27bf1444771aa026b57b67c0580c6e /printing | |
| parent | 0af598b77a6242d796c66884477a046448ef1e21 (diff) | |
Moving Print Ltac to an EXTEND based command.
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppvernac.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 88bb805a72..edd32e8337 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -455,8 +455,6 @@ module Make keyword "Print TypeClasses" | PrintInstances qid -> keyword "Print Instances" ++ spc () ++ pr_smart_global qid - | PrintLtac qid -> - keyword "Print Ltac" ++ spc() ++ pr_ltac_ref qid | PrintCoercions -> keyword "Print Coercions" | PrintCoercionPaths (s,t) -> |