diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-12 13:29:16 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-03 13:37:56 +0200 |
| commit | 4361c1ed9ac5646055f9f0eecc4a003d720c1994 (patch) | |
| tree | 773a5acaa5099e447eca5a62bd9d3e478a4a8e89 /test-suite/success | |
| parent | e9b745af47ba3386724b874e3fd74b6dad33b015 (diff) | |
Type@{_} should not produce a flexible algebraic universe.
Otherwise [(fun x => x) (Type : Type@{_})] becomes
[(fun x : Type@{i+1} => x) (Type@{i} : Type@{i+1})]
breaking the invariant that terms do not contain algebraic universes
(at the lambda abstraction).
Diffstat (limited to 'test-suite/success')
| -rw-r--r-- | test-suite/success/polymorphism.v | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index 0a58fe89a..66ff55edc 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@{_ _}. |