]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed and further code semplification in management of universes.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 17 May 2008 12:59:39 +0000 (12:59 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sat, 17 May 2008 12:59:39 +0000 (12:59 +0000)
helm/software/components/ng_kernel/nCicEnvironment.ml

index ddfe2ca52361506466db29377d5a3be13bd705ea..c2de425c6fbcf4a5bc046f0fd7794619df5012dc 100644 (file)
@@ -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 ||