Merge PR#393: Replace Typeops with Fast_typeops

1 files changed, 3 insertions, 15 deletions

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 81fd1427d0..007acae604 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -15,7 +15,7 @@ open Declarations
 
 (** {6 Typing functions (not yet tagged as safe) }
 
-    They return unsafe judgments that are "in context" of a set of 
+    They return unsafe judgments that are "in context" of a set of
     (local) universe variables (the ones that appear in the term)
     and associated constraints. In case of polymorphic definitions,
     these variables and constraints will be generalized.
@@ -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,24 +98,15 @@ val judge_of_case : env -> case_info
   -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array
     -> unsafe_judgment
 
-(** Typecheck general fixpoint (not checking guard conditions) *)
-val type_fixpoint : env -> Name.t array -> types array
-    -> unsafe_judgment array -> unit
-
-val type_of_constant : env -> pconstant -> types constrained
-
 val type_of_constant_type : env -> constant_type -> types
 
-val type_of_projection : env -> Names.projection puniverses -> types
+val type_of_projection_constant : env -> Names.projection puniverses -> types
 
 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
 
@@ -127,4 +115,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
   constant_type
 
 (** Check that hyps are included in env and fails with error otherwise *)
-val check_hyps_inclusion : env -> constr -> Context.Named.t -> unit
+val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit