+(* *)
+(* 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 *)
+val set_type_checking_info :
+ ?replace_ugraph:(CicUniv.universe_graph option) -> UriManager.uri -> unit