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
-