diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-09-30 18:31:17 +0200 |
|---|---|---|
| committer |  Matthieu Sozeau <mattam@mattam.org> | 2015-10-02 15:54:12 +0200 |
| commit | 42dd4e73346e29db2fe586234b00ca79bd207a5a (patch) | |
| tree | 16260a9dc1dd5974ef34c5eebd37872b5e5aa5ed | |
| parent | e5cbf1ef44449f60eec3bb3c52d08b2943283279 (diff) | |
Univs: fix inference of the lowest sort for records.
| -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 |