diff options
| author | Hugo Herbelin | 2018-02-13 12:19:47 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-13 12:22:34 +0100 |
| commit | 50c948480647af3c5aaea5f80fa9f3341471f2b0 (patch) | |
| tree | 26f18a3c560197dede4932f02b4ac4d8a4acc701 /vernac | |
| parent | d2fb531761e1f4fa02d0c7e7b5b51febe48e357e (diff) | |
Fixing an anomaly in the presence of "let-in" in the type of a record.
Was raised by Jason on Gitter.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/record.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index d9af5378f4..95bcaf6dc3 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -121,7 +121,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 |