Extend Fast_typeops to be a replacement for Typeops

This brings the fix in cad44fc for #2996 to the copy of
Fast_typeops.check_hyps_inclusion.

Fast_typeops.constant_type checks the universe constraints instead of
outputting them. Since everyone who used Typeops.constant_type just
discarded the constraints they've been switched to constant_type_in
which should be the same in Fast_typeops and Typeops.

There are some small differences in the interfaces:
- Typeops.type_of_projection <->
  Fast_typeops.type_of_projection_constant to avoid collision with the
  internally used type_of_projection (which gives the type of [Proj(p,c)]).
- check_hyps_inclusion takes [('a -> constr)] and ['a] instead of
  [constr] for reporting errors.

1 files changed, 5 insertions, 5 deletions

diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index 81fd1427d..cfc82c158 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -102,10 +102,10 @@ val judge_of_case : env -> case_info
     -> unsafe_judgment
 
 (** Typecheck general fixpoint (not checking guard conditions) *)
-val type_fixpoint : env -> Name.t array -> types array
-    -> unsafe_judgment array -> unit
+(* 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 : env -> pconstant -> types constrained *)
 
 val type_of_constant_type : env -> constant_type -> types
 
@@ -116,8 +116,8 @@ 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 : *)
+(*   env -> pconstant -> types Lazy.t array -> types constrained *)
 
 val type_of_constant_knowing_parameters_in :
   env -> pconstant -> types Lazy.t array -> types