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=699af7847a029b05345ef2c49817561ca92a6e59;hb=ca1359de73c1c9deda30c9aaff2606b8dd5253bc;hp=d3ae5c960f5169531f952b43bcbf86d15d1b930d;hpb=fcdc755773839176c7206b579b6dd1ff665ed8f5;p=helm.git

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index d3ae5c960..699af7847 100644
--- a/helm/software/components/cic/cicUniv.ml
+++ b/helm/software/components/cic/cicUniv.ml
@@ -486,7 +486,8 @@ let fresh ?uri ?id () =
 let name_universe u uri =
   match u with
   | (i, None) -> (i, Some uri)
-  | (i, Some ouri) -> 
+  | (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 *)