From 09e15424aab082fd4b18a06e8894227beddeb487 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 May 2017 18:28:10 +0200
Subject: 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.
---
 vernac/record.ml | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'vernac')

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
-- 
cgit v1.2.3