]> matita.cs.unibo.it Git - helm.git/commitdiff
Serious bug fixed: the max of two universes was computed using the polymorphic
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 18 May 2008 07:52:55 +0000 (07:52 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Sun, 18 May 2008 07:52:55 +0000 (07:52 +0000)
max function of OCaml instead of append!!!

helm/software/components/ng_kernel/nCicTypeChecker.ml

index 65e87e55d0c43fd912d53c41a5fb19fd8139ed6a..bccf753f2dff61bb9d3d4ae7f18f8a096b229c04 100644 (file)
@@ -124,7 +124,7 @@ let sort_of_prod ~metasenv ~subst context (name,s) (t1, t2) =
    let t2 = R.whd ~subst ((name,C.Decl s)::context) t2 in
    match t1, t2 with
    | C.Sort s1, C.Sort C.Prop -> t2
-   | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (max u1 u2)) 
+   | C.Sort (C.Type u1), C.Sort (C.Type u2) -> C.Sort (C.Type (u1@u2)) 
    | C.Sort _,C.Sort (C.Type _) -> t2
    | C.Sort (C.Type _) , C.Sort C.CProp -> t1
    | C.Sort _, C.Sort C.CProp