diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 4a2bfaa8b..60fe76bb8 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -141,7 +141,10 @@ let typecheck_params_and_fields def id pl t ps nots fs = else let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in if Univ.is_small_univ univ then - mkArity (ctx, Sorts.sort_of_univ univ), evars + (* We can assume that the level aritysort is not constrained + and clear it. *) + mkArity (ctx, Sorts.sort_of_univ univ), + Evd.set_eq_sort env_ar evars (Prop Pos) aritysort else arity, evars in let evars, nf = Evarutil.nf_evars_and_universes evars in |