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