diff options
Diffstat (limited to 'toplevel/record.ml')
| -rw-r--r-- | toplevel/record.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/toplevel/record.ml b/toplevel/record.ml index 929505716..96221b742 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -121,6 +121,7 @@ let typecheck_params_and_fields def id pl t ps nots fs = | CSort (_, Misctypes.GType []) -> true | _ -> false in let s = interp_type_evars env evars ~impls:empty_internalization_env t in let sred = Reductionops.whd_all env !evars (EConstr.of_constr s) in + let sred = EConstr.Unsafe.to_constr sred in (match kind_of_term sred with | Sort s' -> (if poly then |