-(* Since the universes are not exported directly, but generated *)
-(* typecheking the library, we can't find them in the library as we *)
-(* do for the types. This means that when we commit uris during *)
-(* univ generation we can't associate the uri with the universe graph *)
-(* we find in the library, we have to calculate it and then inject it *)
-(* in the cacke. This is an orrible backdoor used by univ_maker. *)
-(* see the .ml file for some reassuring invariants *)
-(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
-val set_type_checking_info :
- ?replace_ugraph_and_univlist:
- ((CicUniv.universe_graph * CicUniv.universe list) option) ->
- UriManager.uri -> unit
+(* WARNING: THIS FUNCTION MUST BE CALLED ONLY BY CicTypeChecker *)
+val set_type_checking_info : UriManager.uri ->
+ (Cic.obj * CicUniv.universe_graph * CicUniv.universe list) -> unit