assertion was wrong, an object can contain a named univers if its uri is the one...

[helm.git] / helm / software / components / cic / cicUniv.ml

diff --git a/helm/software/components/cic/cicUniv.ml b/helm/software/components/cic/cicUniv.ml
index d3ae5c960f5169531f952b43bcbf86d15d1b930d..699af7847a029b05345ef2c49817561ca92a6e59 100644 (file)
--- 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 *)