aboutsummaryrefslogtreecommitdiffhomepage
path: root/printing/ppconstr.ml
diff options
context:
space:
mode:
Diffstat (limited to 'printing/ppconstr.ml')
-rw-r--r--printing/ppconstr.ml4
1 files changed, 0 insertions, 4 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 38eeda9b9..3041ac259 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -212,10 +212,6 @@ let tag_var = tag Tag.variable
| Some (_,ExplByName id) ->
str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")"
- let pr_opt_type pr = function
- | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
- | t -> cut () ++ str ":" ++ pr t
-
let pr_opt_type_spc pr = function
| CHole (_,_,Misctypes.IntroAnonymous,_) -> mt ()
| t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t