diff options
Diffstat (limited to 'printing/pptactic.ml')
| -rw-r--r-- | printing/pptactic.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7800f1edb..a5716279f 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -685,11 +685,6 @@ module Make | l -> spc () ++ hov 2 (keyword "using" ++ spc () ++ prlist_with_sep pr_comma prc l) - let string_of_debug = function - | Off -> "" - | Debug -> "debug " - | Info -> "info_" - let pr_then () = str ";" let ltop = (5,E) |