From 15bc0d34ae5f72cb31ec383e1ac48ad53f06a725 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sun, 18 May 2008 07:52:55 +0000 Subject: [PATCH] Serious bug fixed: the max of two universes was computed using the polymorphic max function of OCaml instead of append!!! --- helm/software/components/ng_kernel/nCicTypeChecker.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_kernel/nCicTypeChecker.ml b/helm/software/components/ng_kernel/nCicTypeChecker.ml index 65e87e55d..bccf753f2 100644 --- a/helm/software/components/ng_kernel/nCicTypeChecker.ml +++ b/helm/software/components/ng_kernel/nCicTypeChecker.ml @@ -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 -- 2.39.2