Handle mutual records in upper layers.

2 files changed, 22 insertions, 21 deletions

diff --git a/interp/declare.ml b/interp/declare.ml
index e79cc6079..fcb62ac8c 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -383,13 +383,12 @@ let inInductive : inductive_obj -> obj =
     rebuild_function = infer_inductive_subtyping }
 
 let declare_projections univs mind =
-  (** FIXME: handle mutual records *)
-  let mind = (mind, 0) in
   let env = Global.env () in
-  let spec,_ = Inductive.lookup_mind_specif env mind in
-    match spec.mind_record with
-    | PrimRecord info ->
-      let _, kns, _ = info.(0) in
+  let mib = Environ.lookup_mind mind env in
+  match mib.mind_record with
+  | PrimRecord info ->
+    let iter i (_, kns, _) =
+      let mind = (mind, i) in
       let projs = Inductiveops.compute_projections env mind in
       Array.iter2 (fun kn (term, types) ->
 	let id = Label.to_id (Constant.label kn) in
@@ -411,10 +410,12 @@ let declare_projections univs mind =
         let entry = definition_entry ~types ~univs term in
         let kn' = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
         assert (Constant.equal kn kn')
-      ) kns projs;
-      true, true
-    | FakeRecord -> true,false
-    | NotRecord -> false,false
+      ) kns projs
+    in
+    let () = Array.iteri iter info in
+    true, true
+  | FakeRecord -> true, false
+  | NotRecord -> false, false
 
 (* for initial declaration *)
 let declare_mind mie =
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d599afe69..efb205182 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -465,22 +465,21 @@ let build_branch_type env sigma dep p cs =
 let compute_projections env (kn, i as ind) =
   let open Term in
   let mib = Environ.lookup_mind kn env in
-  let indu = match mib.mind_universes with
-  | Monomorphic_ind _ -> mkInd ind
-  | Polymorphic_ind ctx -> mkIndU (ind, make_abstract_instance ctx)
-  | Cumulative_ind ctx ->
-    mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx))
+  let u = match mib.mind_universes with
+  | Monomorphic_ind _ -> Instance.empty
+  | Polymorphic_ind auctx -> make_abstract_instance auctx
+  | Cumulative_ind acumi ->
+    make_abstract_instance (ACumulativityInfo.univ_context acumi)
   in
   let x = match mib.mind_record with
   | NotRecord | FakeRecord ->
     anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
   | PrimRecord info-> Name (pi1 (info.(i)))
   in
-  (** FIXME: handle mutual records *)
-  let pkt = mib.mind_packets.(0) in
-  let { mind_consnrealargs; mind_consnrealdecls } = pkt in
+  let pkt = mib.mind_packets.(i) in
   let { mind_nparams = nparamargs; mind_params_ctxt = params } = mib in
-  let rctx, _ = decompose_prod_assum (subst1 indu pkt.mind_nf_lc.(0)) in
+  let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
+  let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
   let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
   let mp, dp, l = MutInd.repr3 kn in
   (** We build a substitution smashing the lets in the record parameters so
@@ -489,6 +488,7 @@ let compute_projections env (kn, i as ind) =
   let indty =
     (* [ty] = [Ind inst] is typed in context [params] *)
     let inst = Context.Rel.to_extended_vect mkRel 0 paramslet in
+    let indu = mkIndU (ind, u) in
     let ty = mkApp (indu, inst) in
     (* [Ind inst] is typed in context [params-wo-let] *)
     ty
@@ -498,8 +498,8 @@ let compute_projections env (kn, i as ind) =
       { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
       { ci_ind     = ind;
         ci_npar    = nparamargs;
-        ci_cstr_ndecls = mind_consnrealdecls;
-        ci_cstr_nargs = mind_consnrealargs;
+        ci_cstr_ndecls = pkt.mind_consnrealdecls;
+        ci_cstr_nargs = pkt.mind_consnrealargs;
         ci_pp_info = print_info }
   in
   let len = List.length ctx in