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/modules/obj.v | |
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/modules/obj.v')
0 files changed, 0 insertions, 0 deletions