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 893e514b1fef9f642a212997aa92e54be2c0533c..912dad936ed5e042569a7a95004ebd6f1c3c4c2b 100644 (file)
--- 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