From ca1359de73c1c9deda30c9aaff2606b8dd5253bc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 18 Apr 2008 15:27:39 +0000 Subject: [PATCH] assertion was wrong, an object can contain a named univers if its uri is the one of the object itself --- helm/software/components/cic/cicUniv.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 *) -- 2.39.2