Bug fixed and further code semplification in management of universes.

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index ddfe2ca52361506466db29377d5a3be13bd705ea..c2de425c6fbcf4a5bc046f0fd7794619df5012dc 100644 (file)
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -20,10 +20,9 @@ let type0 = [false, NUri.uri_of_string ("cic:/matita/pts/Type.univ")]
 
 let le_constraints = ref [] (* strict,a,b *)
 
-let rec le_path_uri strict a b = 
+let rec le_path_uri strict a b =
  if strict then
-  List.exists (fun (strict,x,y) -> NUri.eq y b &&
-   if strict then le_path_uri false a x else le_path_uri strict a x)
+  List.exists (fun (strict,x,y) -> NUri.eq y b && le_path_uri (not strict) a x)
     !le_constraints
  else
   NUri.eq a b ||