From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 14 Oct 2009 09:37:50 +0000 (+0000)
Subject: Serious bug fixed: fix_sorts used to allow inference of Type[0]:Type[0]!
X-Git-Tag: make_still_working~3309
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=da0c52aa34feaacdcefdf67df433ebbc367fdbc2;p=helm.git

Serious bug fixed: fix_sorts used to allow inference of Type[0]:Type[0]!
---

diff --git a/helm/software/components/ng_kernel/nCicEnvironment.ml b/helm/software/components/ng_kernel/nCicEnvironment.ml
index 893e514b1..912dad936 100644
--- a/helm/software/components/ng_kernel/nCicEnvironment.ml
+++ b/helm/software/components/ng_kernel/nCicEnvironment.ml
@@ -176,8 +176,9 @@ let sup l =
   match l with
   | [(`Type|`CProp),_] -> Some l
   | l ->
-   let bigger_than acc (_s1,n1) = 
-     List.filter (fun x -> lt_path_uri [] n1 x || NUri.eq n1 x) acc 
+   let bigger_than acc (s1,n1) = 
+    List.filter
+     (fun x -> lt_path_uri [] n1 x || (s1 <> `Succ && NUri.eq n1 x)) acc 
    in
    let solutions = List.fold_left bigger_than !universes l in
    let fam = match l with (`CProp,_)::_ -> `CProp | _ -> `Type in