diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 10:09:53 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-03-06 10:09:53 +0100 |
| commit | db8fcbb7763ac784f7c72b72509d5dc7c2c5323c (patch) | |
| tree | 44b43bcbdec48ac23a458e2c525e9a716592b4aa | |
| parent | ddc9728030a98b03447e321d2eb4af0d92add11f (diff) | |
| parent | 50c948480647af3c5aaea5f80fa9f3341471f2b0 (diff) | |
Merge PR #6749: Fixing an anomaly in the presence of "let-in" in the type of a record.
| -rw-r--r-- | test-suite/success/Inductive.v | 6 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
2 files changed, 7 insertions, 1 deletions
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v index 893d75b77..5b1482fd5 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -200,3 +200,9 @@ Module NonRecLetIn. (fun n b c => f_equal (Rec n) eq_refl) 0 (Rec 0 (Base 1)). End NonRecLetIn. + +(* Test treatment of let-in in the definition of Records *) +(* Should fail with "Sort expected" *) + +Fail Inductive foo (T : Type) : let T := Type in T := + { r : forall x : T, x = x }. diff --git a/vernac/record.ml b/vernac/record.ml index 1991a8640..e21f53f55 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -124,7 +124,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = match t with | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in - let sred = Reductionops.whd_all env sigma s in + let sred = Reductionops.whd_allnolet env sigma s in (match EConstr.kind sigma sred with | Sort s' -> let s' = EConstr.ESorts.kind sigma s' in |