*)
(* 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
Cic.term -> CicUniv.universe_graph ->
Cic.term * CicUniv.universe_graph
-(* does_not_occur context lower upper term *)
-(* searches for a Cic.Rel i in term with lower < i <= upper *)
-val does_not_occur : Cic.context -> int -> int -> Cic.term -> bool
-
(* typechecks the obj and puts it in the environment *)
val typecheck_obj : UriManager.uri -> Cic.obj -> unit
-