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.
---
 test-suite/bugs/closed/5233.v  | 2 ++
 test-suite/success/coindprim.v | 9 +++++----
 vernac/record.ml               | 3 +++
 3 files changed, 10 insertions(+), 4 deletions(-)
 create mode 100644 test-suite/bugs/closed/5233.v

diff --git a/test-suite/bugs/closed/5233.v b/test-suite/bugs/closed/5233.v
new file mode 100644
index 0000000000..06286c740d
--- /dev/null
+++ b/test-suite/bugs/closed/5233.v
@@ -0,0 +1,2 @@
+(* Implicit arguments on type were missing for recursive records *)
+Inductive foo {A : Type} : Type := { Foo : foo }.
diff --git a/test-suite/success/coindprim.v b/test-suite/success/coindprim.v
index 5b9265b6a8..05ab913932 100644
--- a/test-suite/success/coindprim.v
+++ b/test-suite/success/coindprim.v
@@ -13,9 +13,10 @@ Definition eta {A} (s : Stream A) := {| hd := s.(hd); tl := s.(tl) |}.
 CoFixpoint ones := {| hd := 1; tl := ones |}.
 CoFixpoint ticks := {| hd := tt; tl := ticks |}.
 
-CoInductive stream_equiv {A} {s : Stream A} {s' : Stream A} : Prop :=
-  mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv _ s.(tl) s'.(tl) }.
-Arguments stream_equiv {A} s s'.
+CoInductive stream_equiv {A} (s : Stream A) (s' : Stream A) : Prop :=
+  mkStreamEq { hdeq : s.(hd) = s'.(hd); tleq : stream_equiv s.(tl) s'.(tl) }.
+Arguments hdeq {A} {s} {s'}.
+Arguments tleq {A} {s} {s'}.
 
 Program CoFixpoint ones_eq : stream_equiv ones ones.(tl) :=
   {| hdeq := eq_refl; tleq := ones_eq |}.
@@ -88,4 +89,4 @@ Lemma eq (x : U) : x = force x.
 Proof.
   Fail destruct x.
 Abort.
-  (* Impossible *)
\ No newline at end of file
+  (* Impossible *)
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