diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 2 | ||||
| -rw-r--r-- | printing/pptactic.ml | 5 |
2 files changed, 0 insertions, 7 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index d15c3ee2f1..c07057a096 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -136,8 +136,6 @@ end) = struct let pr_sep_com sep f c = pr_with_comments (constr_loc c) (sep() ++ f c) - let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" - let pr_univ l = match l with | [_,x] -> str x diff --git a/printing/pptactic.ml b/printing/pptactic.ml index 7800f1edb3..a5716279f3 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) |