diff options
Diffstat (limited to 'vernac/record.ml')
| -rw-r--r-- | vernac/record.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 202c9b92f..2d7800827 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -164,8 +164,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then (* We can assume that the level in aritysort is not constrained and clear it, if it is flexible *) - Evd.set_eq_sort env_ar sigma (Prop Pos) sort, - EConstr.mkSort (Sorts.sort_of_univ univ) + Evd.set_eq_sort env_ar sigma Set sort, EConstr.mkSort (Sorts.sort_of_univ univ) else sigma, typ in let sigma = Evd.minimize_universes sigma in |