aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/pretyping.ml
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-12 13:29:16 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-05-03 13:37:56 +0200
commit4361c1ed9ac5646055f9f0eecc4a003d720c1994 (patch)
tree773a5acaa5099e447eca5a62bd9d3e478a4a8e89 /pretyping/pretyping.ml
parente9b745af47ba3386724b874e3fd74b6dad33b015 (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 'pretyping/pretyping.ml')
-rw-r--r--pretyping/pretyping.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 767e4be35..4886423bd 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