let name_universe u uri =
match u with
| (i, None) -> (i, Some uri)
- | (i, Some ouri) when UriManager.eq ouri uri -> u
- | (i, Some ouri) ->
- (* inside obj living at uri 'uri' should live only
- * universes with uri None. Call Unshare.unshare ~fresh_univs:true
- * if you want to reuse a Type in another object *)
- prerr_endline ("Offending universe: " ^ string_of_universe u^
- " found inside object " ^ UriManager.string_of_uri uri);
- assert false
+ | u -> u
;;
let print_ugraph (g, _, o) =
Xml.pp ~gzip:true tokens (Some filename)
let univno = fst
+let univuri = function
+ | _,None -> UriManager.uri_of_string "cic:/fake.con"
+ | _,Some u -> u
let rec clean_ugraph m already_contained f =