X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;fp=helm%2Fsoftware%2Fcomponents%2Fcic%2FcicUniv.ml;h=beb8a233fb58b3f56fb516131ca1b14188182bf0;hb=c031aa4ca97d0d563a772d7bd247ff7814c51b04;hp=a936c16bf9fb688e399cb5e30c63fe6813323644;hpb=6c7be6bbe4e645f5ab99e82d322e1a70503781cb;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index a936c16bf..beb8a233f 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -380,14 +380,7 @@ let fresh ?uri ?id () =
 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) = 
@@ -636,6 +629,9 @@ let write_xml_of_ugraph filename (m,_,_) l =
     Xml.pp ~gzip:true tokens (Some filename)
 
 let univno = fst
+let univuri = function 
+  | _,None -> assert false
+  | _,Some u -> u
 
  
 let rec clean_ugraph m already_contained f =