From 90b6969c467f097a4d7da0140e1351ef98d6401d Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 28 Jan 2017 14:11:50 +0100
Subject: Remove useless comments

---
 kernel/typeops.mli | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'kernel')

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 73c63db681..007acae604 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -91,9 +91,6 @@ val judge_of_cast :
 
 val judge_of_inductive : env -> inductive puniverses -> unsafe_judgment
 
-(* val judge_of_inductive_knowing_parameters : *)
-(*   env -> inductive -> unsafe_judgment array -> unsafe_judgment *)
-
 val judge_of_constructor : env -> constructor puniverses -> unsafe_judgment
 
 (** {6 Type of Cases. } *)
@@ -101,8 +98,6 @@ val judge_of_case : env -> case_info
   -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
     -> unsafe_judgment
 
-(* val type_of_constant : env -> pconstant -> types constrained *)
-
 val type_of_constant_type : env -> constant_type -> types
 
 val type_of_projection_constant : env -> Names.projection puniverses -> types
@@ -112,9 +107,6 @@ val type_of_constant_in : env -> pconstant -> types
 val type_of_constant_type_knowing_parameters :
   env -> constant_type -> types Lazy.t array -> types
 
-(* val type_of_constant_knowing_parameters : *)
-(*   env -> pconstant -> types Lazy.t array -> types constrained *)
-
 val type_of_constant_knowing_parameters_in :
   env -> pconstant -> types Lazy.t array -> types
 
-- 
cgit v1.2.3