From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 printing/ppconstr.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'printing/ppconstr.ml')

diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 38eeda9b96..3041ac259e 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
-- 
cgit v1.2.3