diff options
| -rw-r--r-- | pretyping/pretyping.ml | 3 | ||||
| -rw-r--r-- | test-suite/success/polymorphism.v | 10 |
2 files changed, 7 insertions, 6 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 767e4be35b..4886423bd0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -229,7 +229,8 @@ let interp_universe ?loc evd = function evd, Univ.Universe.make l | l -> List.fold_left (fun (evd, u) l -> - let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible_alg evd l in + (* [univ_flexible_alg] can produce algebraic universes in terms *) + let evd', l = interp_universe_level_name ~anon_rigidity:univ_flexible evd l in (evd', Univ.sup u (Univ.Universe.make l))) (evd, Univ.Universe.type0m) l diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 0a58fe89a1..66ff55edcb 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -333,12 +333,12 @@ Module Anonymous. Definition anonid := (fun x => x) : Type -> Type@{_}. Check anonid@{_}. - Definition defaultalg := Type : Type. - Definition usedefaultalg := defaultalg@{_ _}. + Definition defaultalg := (fun x : Type => x) (Type : Type). + Definition usedefaultalg := defaultalg@{_ _ _}. Check usedefaultalg@{_ _}. - Definition anonalg := (fun x => x) (Type : Type@{_}). - Check anonalg@{_}. + Definition anonalg := (fun x : Type@{_} => x) (Type : Type). + Check anonalg@{_ _}. Definition unrelated@{i j} := nat. Definition useunrelated := unrelated@{_ _}. @@ -346,7 +346,7 @@ Module Anonymous. Definition inthemiddle@{i j k} := let _ := defaultid@{i j} in - defaultalg@{k j}. + anonalg@{k j}. (* i <= j < k *) Definition collapsethemiddle := inthemiddle@{i _ j}. Check collapsethemiddle@{_ _}. |