diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2016-03-14 19:50:29 +0100 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2016-03-15 15:28:13 +0100 |
| commit | 779fd5d9a4982b19fd257b61f444ae8e6155dcbe (patch) | |
| tree | 9073f67d279fa70732cc7ac2f1dde846e37175bf | |
| parent | e171456870f9893d582d53114d4f87e634c007e5 (diff) | |
Fix bug when a sort is ascribed to a Record
Forcefully equating it to the inferred level is not always desirable or possible.
| -rw-r--r-- | test-suite/success/univers.v | 17 | ||||
| -rw-r--r-- | toplevel/record.ml | 13 |
2 files changed, 24 insertions, 6 deletions
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index e00701fb6..269359ae6 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -60,3 +60,20 @@ Qed. (* Submitted by Danko Ilik (bug report #1507); related to LetIn *) Record U : Type := { A:=Type; a:A }. + +(** Check assignement of sorts to inductives and records. *) + +Variable sh : list nat. + +Definition is_box_in_shape (b :nat * nat) := True. +Definition myType := Type. + +Module Ind. +Inductive box_in : myType := + myBox (coord : nat * nat) (_ : is_box_in_shape coord) : box_in. +End Ind. + +Module Rec. +Record box_in : myType := + BoxIn { coord :> nat * nat; _ : is_box_in_shape coord }. +End Rec.
\ No newline at end of file diff --git a/toplevel/record.ml b/toplevel/record.ml index 04da628c3..200d1a938 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -140,12 +140,13 @@ let typecheck_params_and_fields def id pl t ps nots fs = arity, evars else let evars = Evd.set_leq_sort env_ar evars (Type univ) aritysort in - if Univ.is_small_univ univ then - (* 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 + if Univ.is_small_univ univ && + Option.cata (Evd.is_flexible_level evars) false (Evd.is_sort_variable evars aritysort) then + (* We can assume that the level in aritysort is not constrained + and clear it, if it is flexible *) + 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 let newps = map_rel_context nf newps in |