Fix primitive projections declarations for inductive records.

2 files changed, 36 insertions, 2 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 759d712061..2e9a81d98f 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -781,16 +781,17 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
     match isrecord with
     | Some true when pkt.mind_kelim == all_sorts && Array.length pkt.mind_consnames == 1 ->
       (** The elimination criterion ensures that all projections can be defined. *)
-      let rctx, _ = decompose_prod_assum pkt.mind_nf_lc.(0) in
       let u = 
 	if p then 
 	  subst_univs_level_instance subst (Univ.UContext.instance ctx)
 	else Univ.Instance.empty 
       in
+      let indsp = ((kn, 0), u) in
+      let rctx, _ = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
 	(try 
 	   let fields = List.firstn pkt.mind_consnrealdecls.(0) rctx in
 	   let kns, projs = 
-	     compute_projections ((kn, 0), u) pkt.mind_typename nparamargs params
+	     compute_projections indsp pkt.mind_typename nparamargs params
 	       pkt.mind_consnrealdecls pkt.mind_consnrealargs fields
 	   in Some (kns, projs)
 	 with UndefinableExpansion -> Some ([||], [||]))
diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v
index 2682df3b72..4a9c81eb3b 100644
--- a/test-suite/success/primitiveproj.v
+++ b/test-suite/success/primitiveproj.v
@@ -28,3 +28,36 @@ Section bla.
 End bla.
 
 End Univ.
+
+Set Primitive Projections.
+Unset Elimination Schemes.
+Set Implicit Arguments.
+
+Check nat.
+
+(* Inductive X (U:Type) := Foo (k : nat) (x : X U).  *)
+(* Parameter x : X nat. *)
+(* Check x.(k). *)
+
+Inductive X (U:Type) := { k : nat; a: k = k -> X U; b : let x := a eq_refl in X U }.
+
+Parameter x:X nat.
+Check (a x : forall _ : @eq nat (k x) (k x), X nat).
+Check (b x : X nat).
+
+Inductive Y := { next : option Y }.
+
+Check _.(next) : option Y.
+Lemma eta_ind (y : Y) : y = Build_Y y.(next).
+Proof. reflexivity. Defined.
+
+Variable t : Y.
+
+Fixpoint yn (n : nat) (y : Y) : Y := 
+  match n with
+    | 0 => t
+    | S n => {| next := Some (yn n y) |}
+  end.
+
+Lemma eta_ind'  (y: Y) : Some (yn 100 y) = Some {| next := (yn 100 y).(next) |}.
+Proof. reflexivity. Defined.