From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 18 Apr 2008 15:27:39 +0000 (+0000)
Subject: assertion was wrong, an object can contain a named univers if its uri is the one... 
X-Git-Tag: make_still_working~5323
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=ca1359de73c1c9deda30c9aaff2606b8dd5253bc;p=helm.git

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

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 *)