From da0c52aa34feaacdcefdf67df433ebbc367fdbc2 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 14 Oct 2009 09:37:50 +0000 Subject: [PATCH] Serious bug fixed: fix_sorts used to allow inference of Type[0]:Type[0]! --- helm/software/components/ng_kernel/nCicEnvironment.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) 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 -- 2.39.2