Cic.term -> CicUniv.universe_graph ->
Cic.term * CicUniv.universe_graph
-(* typechecks the obj and puts it in the environment *)
+(* typechecks the obj and puts it in the environment
+ * empty universes are filed with the given uri, thus you should
+ * get the object again after calling this *)
val typecheck_obj : UriManager.uri -> Cic.obj -> unit
(* check_allowed_sort_elimination uri i s1 s2