diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/record.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/vernac/record.ml b/vernac/record.ml index 3984f4509d..a220e515e7 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -137,6 +137,9 @@ let typecheck_params_and_fields def id pl t ps nots fs = in let arity = EConstr.it_mkProd_or_LetIn typ newps in let env_ar = EConstr.push_rel_context newps (EConstr.push_rel (LocalAssum (Name id,arity)) env0) in + let assums = List.filter is_local_assum newps in + let params = List.map (RelDecl.get_name %> out_name) assums in + let impls_env = compute_internalization_env env0 ~impls:impls_env (Inductive params) [id] [EConstr.to_constr !evars arity] [imps] in let env2,impls,newfs,data = interp_fields_evars env_ar evars impls_env nots (binders_of_decls fs) in |