Replace Typeops by Fast_typeops

This is really [mv fast_typeops.ml{,i} typeops.ml{,i}] plus trivial
changes in the other files, the real changes are in the parent commit.

1 files changed, 3 insertions, 7 deletions

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index cfc82c158..73c63db68 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.
@@ -101,15 +101,11 @@ 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
 
@@ -127,4 +123,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