*)
(* These are the only exceptions that will be raised *)
-exception TypeCheckerFailure of string
-exception AssertFailure of string
+exception TypeCheckerFailure of string Lazy.t
+exception AssertFailure of string Lazy.t
val debrujin_constructor : UriManager.uri -> int -> Cic.term -> Cic.term
(* 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