Fixing #5233 (missing implicit arguments for recursive records).

Was failing e.g. with

Inductive foo {A : Type} : Type := { Foo : foo }.

Note: the test-suite was using the bug in coindprim.v.

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