+ ?subst:Cic.substitution -> Cic.metasenv -> Cic.context ->
+ Cic.term -> CicUniv.universe_graph ->
+ Cic.term * CicUniv.universe_graph
+
+(* typechecks the obj and puts it in the environment *)
+val typecheck_obj : UriManager.uri -> Cic.obj -> unit
+
+(* check_allowed_sort_elimination uri i s1 s2
+ This function is used outside the kernel to determine in advance whether
+ a MutCase will be allowed or not.
+ [uri,i] is the type of the term to match
+ [s1] is the sort of the term to eliminate (i.e. the head of the arity
+ of the inductive type [uri,i])
+ [s2] is the sort of the goal (i.e. the head of the type of the outtype
+ of the MutCase) *)
+val check_allowed_sort_elimination:
+ UriManager.uri -> int -> Cic.sort -> Cic.sort -> bool