diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 3 |
1 files changed, 2 insertions, 1 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 |