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
+