From 14684f9b8fcc2ce4ffb0b9fa5d287c2ab5843760 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 17 May 2008 12:59:39 +0000 Subject: [PATCH] Bug fixed and further code semplification in management of universes. --- helm/software/components/ng_kernel/nCicEnvironment.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml index ddfe2ca52..c2de425c6 100644 --- 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 || -- 2.39.2