]> matita.cs.unibo.it Git - helm.git/commitdiff
Serious bug fixed: fix_sorts used to allow inference of Type[0]:Type[0]!
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 14 Oct 2009 09:37:50 +0000 (09:37 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 14 Oct 2009 09:37:50 +0000 (09:37 +0000)
helm/software/components/ng_kernel/nCicEnvironment.ml

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