diff options
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) -> |