Using more general information for primitive records.

This brings more compatibility with handling of mutual primitive records
in the kernel.

26 files changed, 129 insertions, 84 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index ee7914f99..a890f2cef 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -252,9 +252,10 @@ type recarg =
 
 type wf_paths = recarg Rtree.t
 
-type record_body = (Id.t * Constant.t array * projection_body array) option
-    (* The body is empty for non-primitive records, otherwise we get its
-       binder name in projections and list of projections if it is primitive. *)
+type record_info =
+| NotRecord
+| FakeRecord
+| PrimRecord of (Id.t * Constant.t array * projection_body array) array
 
 type regular_inductive_arity = {
   mind_user_arity : constr;
@@ -322,7 +323,7 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : record_body option; (** Whether the inductive type has been declared as a record. *)
+    mind_record : record_info; (** Whether the inductive type has been declared as a record. *)
 
     mind_finite : recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
diff --git a/checker/closure.ml b/checker/closure.ml
index b9ae4daa8..2dcc1a984 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -619,7 +619,8 @@ let drop_parameters depth n argstk =
 let eta_expand_ind_stack env ind m s (f, s') =
   let mib = lookup_mind (fst ind) env in
     match mib.mind_record with
-    | Some (Some (_,projs,pbs)) when mib.mind_finite <> CoFinite -> 
+    | PrimRecord info when mib.mind_finite <> CoFinite ->
+      let (_, projs, pbs) = info.(snd ind) in
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.mind_nparams in
diff --git a/checker/environ.ml b/checker/environ.ml
index 3d5fac806..ba1eb0ddb 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -192,11 +192,12 @@ let add_mind kn mib env =
       (MutInd.to_string kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
   let new_projections = match mib.mind_record with
-    | None | Some None -> env.env_globals.env_projections
-    | Some (Some (id, kns, pbs)) ->
-      Array.fold_left2 (fun projs kn pb ->
-          Cmap_env.add kn pb projs)
-        env.env_globals.env_projections kns pbs
+    | NotRecord | FakeRecord -> env.env_globals.env_projections
+    | PrimRecord projs ->
+      Array.fold_left (fun accu (id, kns, pbs) ->
+      Array.fold_left2 (fun accu kn pb ->
+          Cmap_env.add kn pb accu) accu kns pbs)
+        env.env_globals.env_projections projs
   in
   let kn1,kn2 =  MutInd.user kn, MutInd.canonical kn in
   let new_inds_eq = if KerName.equal kn1 kn2 then
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 6a051a5a9..a22af4e0f 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -218,16 +218,19 @@ let check_inductive  env mp1 l info1 mib2 spec2 subst1 subst2=
   (* we check that records and their field names are preserved. *)
   let record_equal x y =
     match x, y with
-    | None, None -> true
-    | Some None, Some None -> true
-    | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) ->
-      Id.equal id1 id2 &&
-      Array.for_all2 Constant.UserOrd.equal p1 p2 &&
-      Array.for_all2 eq_projection_body pb1 pb2
+    | NotRecord, NotRecord -> true
+    | FakeRecord, FakeRecord -> true
+    | PrimRecord info1, PrimRecord info2 ->
+      let check (id1, p1, pb1) (id2, p2, pb2) =
+        Id.equal id1 id2 &&
+        Array.for_all2 Constant.UserOrd.equal p1 p2 &&
+        Array.for_all2 eq_projection_body pb1 pb2
+      in
+      Array.equal check info1 info2
     | _, _ -> false
   in
   check record_equal (fun mib -> mib.mind_record);
-  if mib1.mind_record != None then begin
+  if mib1.mind_record != NotRecord then begin
     let rec names_prod_letin t = match t with
       | Prod(n,_,t) -> n::(names_prod_letin t)
       | LetIn(n,_,_,t) -> n::(names_prod_letin t)
diff --git a/checker/values.ml b/checker/values.ml
index c0ddc1908..4f28d6e44 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -15,7 +15,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 2356846eddb0113e5e75bf8b46cddaee checker/cic.mli
+MD5 42fb0781dc5f7f2cbe3ca127f8249264 checker/cic.mli
 
 *)
 
@@ -274,8 +274,10 @@ let v_one_ind = v_tuple "one_inductive_body"
     Any|]
 
 let v_finite = v_enum "recursivity_kind" 3
-let v_mind_record = Annot ("mind_record", 
-			   Opt (Opt (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |])))
+
+let v_record_info =
+  v_sum "record_info" 2
+    [| [| Array (v_tuple "record" [| v_id; Array v_cst; Array v_projbody |]) |] |]
 
 let v_ind_pack_univs = 
   v_sum "abstract_inductive_universes" 0
@@ -283,7 +285,7 @@ let v_ind_pack_univs =
 
 let v_ind_pack = v_tuple "mutual_inductive_body"
   [|Array v_one_ind;
-    v_mind_record;
+    v_record_info;
     v_finite;
     Int;
     v_section_ctxt;
diff --git a/interp/declare.ml b/interp/declare.ml
index aa737239b..e79cc6079 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -383,11 +383,14 @@ 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,0) in
+  let spec,_ = Inductive.lookup_mind_specif env mind in
     match spec.mind_record with
-    | Some (Some (_, kns, _)) ->
-      let projs = Inductiveops.compute_projections env (mind, 0) in
+    | PrimRecord info ->
+      let _, kns, _ = info.(0) in
+      let projs = Inductiveops.compute_projections env mind in
       Array.iter2 (fun kn (term, types) ->
 	let id = Label.to_id (Constant.label kn) in
         let univs = match univs with
@@ -410,8 +413,8 @@ let declare_projections univs mind =
         assert (Constant.equal kn kn')
       ) kns projs;
       true, true
-    | Some None -> true,false
-    | None -> false,false
+    | FakeRecord -> true,false
+    | NotRecord -> false,false
 
 (* for initial declaration *)
 let declare_mind mie =
diff --git a/interp/discharge.ml b/interp/discharge.ml
index e16a955d9..0e44a8b46 100644
--- a/interp/discharge.ml
+++ b/interp/discharge.ml
@@ -111,9 +111,10 @@ let process_inductive info modlist mib =
   let section_decls' = Context.Named.map discharge section_decls in
   let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
   let record = match mib.mind_record with
-    | Some (Some (id, _, _)) -> Some (Some id)
-    | Some None -> Some None
-    | None -> None
+    | PrimRecord info ->
+      Some (Some (Array.map pi1 info))
+    | FakeRecord -> Some None
+    | NotRecord -> None
   in
   { mind_entry_record = record;
     mind_entry_finite = mib.mind_finite;
diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml
index 74618a290..5bf46282f 100644
--- a/interp/dumpglob.ml
+++ b/interp/dumpglob.ml
@@ -113,7 +113,7 @@ let type_of_global_ref gr =
 	"var" ^ type_of_logical_kind (Decls.variable_kind v)
     | Globnames.IndRef ind ->
 	let (mib,oib) = Inductive.lookup_mind_specif (Global.env ()) ind in
-	  if mib.Declarations.mind_record <> None then
+          if mib.Declarations.mind_record <> Declarations.NotRecord then
             begin match mib.Declarations.mind_finite with
             | Finite -> "indrec"
             | BiFinite -> "rec"
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index c9362bce6..1d5142a5c 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -820,10 +820,12 @@ let drop_parameters depth n argstk =
     constructor is partially applied.
  *)
 let eta_expand_ind_stack env ind m s (f, s') =
+  let open Declarations in
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (Some (_,projs,pbs)) when
+    | PrimRecord infos when
         mib.Declarations.mind_finite == Declarations.BiFinite ->
+      let (_, projs, _) = infos.(snd ind) in
 	(* (Construct, pars1 .. parsm :: arg1...argn :: []) ~= (f, s') ->
 	   arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *)
       let pars = mib.Declarations.mind_nparams in
@@ -834,7 +836,7 @@ let eta_expand_ind_stack env ind m s (f, s') =
       let hstack = Array.map (fun p -> { norm = Red; (* right can't be a constructor though *)
 					 term = FProj (Projection.make p true, right) }) projs in
 	argss, [Zapp hstack]
-    | _ -> raise Not_found (* disallow eta-exp for non-primitive records *)
+    | PrimRecord _ | NotRecord | FakeRecord -> raise Not_found (* disallow eta-exp for non-primitive records *)
 
 let rec project_nth_arg n argstk =
   match argstk with
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index bb81f7514..58fb5d66b 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -109,13 +109,22 @@ v}
 *)
 
 (** Record information:
-    If the record is not primitive, then None
-    Otherwise, we get:
+    If the type is not a record, then NotRecord
+    If the type is a non-primitive record, then FakeRecord
+    If it is a primitive record, for every type in the block, we get:
     - The identifier for the binder name of the record in primitive projections.
     - The constants associated to each projection.
-    - The checked projection bodies. *)
+    - The checked projection bodies.
 
-type record_body = (Id.t * Constant.t array * projection_body array) option
+    The kernel does not exploit the difference between [NotRecord] and
+    [FakeRecord]. It is mostly used by extraction, and should be extruded from
+    the kernel at some point.
+*)
+
+type record_info =
+| NotRecord
+| FakeRecord
+| PrimRecord of (Id.t * Constant.t array * projection_body array) array
 
 type regular_inductive_arity = {
   mind_user_arity : types;
@@ -181,7 +190,7 @@ type mutual_inductive_body = {
 
     mind_packets : one_inductive_body array;  (** The component of the mutual inductive block *)
 
-    mind_record : record_body option; (** The record information *)
+    mind_record : record_info; (** The record information *)
 
     mind_finite : recursivity_kind;  (** Whether the type is inductive or coinductive *)
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index ad5167d8b..3e6c4858e 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -208,14 +208,21 @@ let subst_mind_packet sub mbp =
     mind_nb_args = mbp.mind_nb_args;
     mind_reloc_tbl = mbp.mind_reloc_tbl }
 
-let subst_mind_record sub (id, ps, pb as r) =
-  let ps' = Array.Smart.map (subst_constant sub) ps in
-  let pb' = Array.Smart.map (subst_const_proj sub) pb in
-    if ps' == ps && pb' == pb then r
+let subst_mind_record sub r = match r with
+| NotRecord -> NotRecord
+| FakeRecord -> FakeRecord
+| PrimRecord infos ->
+  let map (id, ps, pb as info) =
+    let ps' = Array.Smart.map (subst_constant sub) ps in
+    let pb' = Array.Smart.map (subst_const_proj sub) pb in
+    if ps' == ps && pb' == pb then info
     else (id, ps', pb')
+  in
+  let infos' = Array.Smart.map map infos in
+  if infos' == infos then r else PrimRecord infos'
 
 let subst_mind_body sub mib =
-  { mind_record = Option.Smart.map (Option.Smart.map (subst_mind_record sub)) mib.mind_record ;
+  { mind_record = subst_mind_record sub mib.mind_record ;
     mind_finite = mib.mind_finite ;
     mind_ntypes = mib.mind_ntypes ;
     mind_hyps = (match mib.mind_hyps with [] -> [] | _ -> assert false);
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 3c555f8c7..724ed9ec7 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -49,9 +49,9 @@ type one_inductive_entry = {
   mind_entry_lc : constr list }
 
 type mutual_inductive_entry = {
-  mind_entry_record : (Id.t option) option; 
-  (** Some (Some id): primitive record with id the binder name of the record
-      in projections.
+  mind_entry_record : (Id.t array option) option;
+  (** Some (Some ids): primitive records with ids the binder name of each
+      record in their respective projections. Not used by the kernel.
       Some None: non-primitive record *)
   mind_entry_finite : Declarations.recursivity_kind;
   mind_entry_params : (Id.t * local_entry) list;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2d6c9117b..0e34a7165 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -515,11 +515,12 @@ let template_polymorphic_pind (ind,u) env =
 let add_mind_key kn (mind, _ as mind_key) env =
   let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in
   let new_projections = match mind.mind_record with
-    | None | Some None -> env.env_globals.env_projections
-    | Some (Some (id, kns, pbs)) ->
-      Array.fold_left2 (fun projs kn pb ->
-          Cmap_env.add kn pb projs)
-        env.env_globals.env_projections kns pbs
+    | NotRecord | FakeRecord -> env.env_globals.env_projections
+    | PrimRecord projs ->
+      Array.fold_left (fun accu (id, kns, pbs) ->
+      Array.fold_left2 (fun accu kn pb ->
+          Cmap_env.add kn pb accu) accu kns pbs)
+        env.env_globals.env_projections projs
   in
   let new_globals =
     { env.env_globals with
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5b3bca3a0..df22e21ad 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -938,6 +938,8 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
     | Some (Some rid) when pkt.mind_kelim == all_sorts
 			   && Array.length pkt.mind_consnames == 1
 			   && pkt.mind_consnrealargs.(0) > 0 ->
+      (** FIXME: adapt to mutual records *)
+      let () = assert (Array.length rid == 1) in
       (** The elimination criterion ensures that all projections can be defined. *)
       let u =
         match aiu with
@@ -949,13 +951,13 @@ let build_inductive env prv iu env_ar paramsctxt kn isrecord isfinite inds nmr r
       let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
 	(try 
 	   let fields, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
-	   let kns, projs = 
+            let kn, projs =
              compute_projections indsp nparamargs paramsctxt
 	       pkt.mind_consnrealdecls pkt.mind_consnrealargs paramslet fields
-	   in Some (Some (rid, kns, projs))
-	 with UndefinableExpansion -> Some None)
-    | Some _ -> Some None
-    | None -> None
+           in PrimRecord [|rid.(0), kn, projs|]
+         with UndefinableExpansion -> FakeRecord)
+    | Some _ -> FakeRecord
+    | None -> NotRecord
   in
     (* Build the mutual inductive *)
     { mind_record = isrecord;
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 090acdf16..9130b8778 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -293,8 +293,8 @@ let elim_sorts (_,mip) = mip.mind_kelim
 let is_private (mib,_) = mib.mind_private = Some true
 let is_primitive_record (mib,_) = 
   match mib.mind_record with
-  | Some (Some _) -> true
-  | _ -> false
+  | PrimRecord _ -> true
+  | NotRecord | FakeRecord -> false
 
 let build_dependent_inductive ind (_,mip) params =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 914168695..6821fc980 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1990,8 +1990,10 @@ let compile_mind prefix ~interactive mb mind stack =
       Glet (gn, mkMLlam [|c_uid|] code) :: acc
     in
     let projs = match mb.mind_record with
-    | None | Some None -> []
-    | Some (Some (id, kns, pbs)) -> Array.fold_left_i add_proj [] pbs
+    | NotRecord | FakeRecord -> []
+    | PrimRecord info ->
+      let _, _, pbs = info.(i) in
+      Array.fold_left_i add_proj [] pbs
     in
     projs @ constructors @ gtype :: accu :: stack
   in
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 8cf588c3e..13701d489 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -226,8 +226,9 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
     else error NotEqualInductiveAliases
   end;
   (* we check that records and their field names are preserved. *)
-  check (fun mib -> mib.mind_record <> None) (==) (fun x -> RecordFieldExpected x);
-  if mib1.mind_record <> None then begin
+  (** FIXME: this check looks nonsense *)
+  check (fun mib -> mib.mind_record <> NotRecord) (==) (fun x -> RecordFieldExpected x);
+  if mib1.mind_record <> NotRecord then begin
     let rec names_prod_letin t = match kind t with
       | Prod(n,_,t) -> n::(names_prod_letin t)
       | LetIn(n,_,_,t) -> n::(names_prod_letin t)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index bbf56525a..71e09992c 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -488,7 +488,7 @@ and extract_really_ind env kn mib =
 	    Int.equal (List.length l) 1 && not (type_mem_kn kn (List.hd l))
 	then raise (I Singleton);
 	if List.is_empty l then raise (I Standard);
-	if Option.is_empty mib.mind_record then raise (I Standard);
+        if mib.mind_record == Declarations.NotRecord then raise (I Standard);
 	(* Now we're sure it's a record. *)
 	(* First, we find its field names. *)
 	let rec names_prod t = match Constr.kind t with
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6d08f66c1..88a91af88 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -984,9 +984,11 @@ and conv_record trs env evd (ctx,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2)
   else UnifFailure(evd,(*dummy*)NotSameHead)
 
 and eta_constructor ts env evd sk1 ((ind, i), u) sk2 term2 =
+  let open Declarations in
   let mib = lookup_mind (fst ind) env in
     match mib.Declarations.mind_record with
-    | Some (Some (id, projs, pbs)) when mib.Declarations.mind_finite == Declarations.BiFinite ->
+    | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite ->
+      let (_, projs, _) = info.(snd ind) in
       let pars = mib.Declarations.mind_nparams in
 	(try 
 	   let l1' = Stack.tail pars sk1 in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1003f86c5..d599afe69 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -277,8 +277,8 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 
 let has_dependent_elim mib =
   match mib.mind_record with
-  | Some (Some _) -> mib.mind_finite == BiFinite
-  | _ -> true
+  | PrimRecord _ -> mib.mind_finite == BiFinite
+  | NotRecord | FakeRecord -> true
 
 (* Annotation for cases *)
 let make_case_info env ind style =
@@ -346,8 +346,10 @@ let get_constructors env (ind,params) =
 let get_projections env (ind,params) =
   let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
     match mib.mind_record with
-    | Some (Some (id, projs, pbs)) -> Some projs
-    | _ -> None
+    | PrimRecord infos ->
+      let (_, projs, _) = infos.(snd (fst ind)) in
+      Some projs
+    | NotRecord | FakeRecord -> None
 
 let make_case_or_project env sigma indf ci pred c branches =
   let open EConstr in
@@ -460,7 +462,7 @@ let build_branch_type env sigma dep p cs =
     build an expansion function.
     The term built is expecting to be substituted first by
     a substitution of the form [params, x : ind params] *)
-let compute_projections env (kn, _ as ind) =
+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
@@ -470,9 +472,9 @@ let compute_projections env (kn, _ as ind) =
     mkIndU (ind, make_abstract_instance (ACumulativityInfo.univ_context ctx))
   in
   let x = match mib.mind_record with
-  | None | Some None ->
+  | NotRecord | FakeRecord ->
     anomaly Pp.(str "Trying to build primitive projections for a non-primitive record")
-  | Some (Some (id, _, _)) -> Name id
+  | PrimRecord info-> Name (pi1 (info.(i)))
   in
   (** FIXME: handle mutual records *)
   let pkt = mib.mind_packets.(0) in
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 4b8e0e096..7319846fb 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -188,12 +188,13 @@ let branch_of_switch lvl ans bs =
     bs ci in
   Array.init (Array.length tbl) branch
 
-let get_proj env ((mind, _n), i) =
+let get_proj env ((mind, n), i) =
   let mib = Environ.lookup_mind mind env in
   match mib.mind_record with
-  | None | Some None ->
+  | NotRecord | FakeRecord ->
     CErrors.anomaly (Pp.strbrk "Return type is not a primitive record")
-  | Some (Some (_, projs, _)) ->
+  | PrimRecord info ->
+    let _, projs, _ = info.(n) in
     Projection.make projs.(i) true
 
 let rec nf_val env sigma v typ =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5cf6e4b26..4ba5d2794 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -656,10 +656,12 @@ let rec is_neutral env sigma ts t =
 
 let is_eta_constructor_app env sigma ts f l1 term =
   match EConstr.kind sigma f with
-  | Construct (((_, i as ind), j), u) when i == 0 && j == 1 ->
+  | Construct (((_, i as ind), j), u) when j == 1 ->
+    let open Declarations in
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (Some (_,exp,projs)) when mib.Declarations.mind_finite == Declarations.BiFinite &&
+      | PrimRecord info when mib.Declarations.mind_finite == Declarations.BiFinite &&
+          let (_, projs, _) = info.(i) in
           Array.length projs == Array.length l1 - mib.Declarations.mind_nparams ->
 	(** Check that the other term is neutral *)
 	is_neutral env sigma ts term
@@ -667,11 +669,13 @@ let is_eta_constructor_app env sigma ts f l1 term =
   | _ -> false
 
 let eta_constructor_app env sigma f l1 term =
+  let open Declarations in
   match EConstr.kind sigma f with
   | Construct (((_, i as ind), j), u) ->
     let mib = lookup_mind (fst ind) env in
       (match mib.Declarations.mind_record with
-      | Some (Some (_, projs, _)) ->
+      | PrimRecord info ->
+        let (_, projs, _) = info.(i) in
         let npars = mib.Declarations.mind_nparams in
 	let pars, l1' = Array.chop npars l1 in
 	let arg = Array.append pars [|term|] in
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 5e5d00362..f926e8275 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -246,13 +246,13 @@ let print_type_in_type ref =
   else []
 
 let print_primitive_record recflag mipv = function
-  | Some (Some (_, ps,_)) ->
+  | PrimRecord _ ->
     let eta = match recflag with
     | CoFinite | Finite -> str" without eta conversion"
     | BiFinite -> str " with eta conversion"
     in
     [Id.print mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
-  | _ -> []
+  | FakeRecord | NotRecord -> []
 
 let print_primitive ref =
   match ref with 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index be8bc1357..3f95dcfb6 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -217,7 +217,7 @@ let print_record env mind mib udecl =
   )
 
 let pr_mutual_inductive_body env mind mib udecl =
-  if mib.mind_record <> None && not !Flags.raw_print then
+  if mib.mind_record != NotRecord && not !Flags.raw_print then
     print_record env mind mib udecl
   else
     print_mutual_inductive env mind mib udecl
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index f34c83ae7..837865e64 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -753,8 +753,8 @@ module New = struct
     let (ind,t) = pf_reduce_to_quantified_ind gl (pf_unsafe_type_of gl c) in
     let isrec,mkelim =
       match (Global.lookup_mind (fst (fst ind))).mind_record with
-      | None -> true,gl_make_elim
-      | Some _ -> false,gl_make_case_dep
+      | NotRecord -> true,gl_make_elim
+      | FakeRecord | PrimRecord _ -> false,gl_make_case_dep
     in
     general_elim_then_using mkelim isrec None tac None ind (c, t)
     end
diff --git a/vernac/record.ml b/vernac/record.ml
index 940859723..a97a1662e 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -292,8 +292,8 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers u
     if !primitive_flag then 
       let is_primitive = 
 	match mib.mind_record with
-	| Some (Some _) -> true
-	| Some None | None -> false
+        | PrimRecord _ -> true
+        | FakeRecord | NotRecord -> false
       in
 	if not is_primitive then 
 	  warn_non_primitive_record (env,indsp);
@@ -403,7 +403,7 @@ let declare_structure finite ubinders univs id idbuild paramimpls params arity t
   in
   let mie =
     { mind_entry_params = List.map degenerate_decl params;
-      mind_entry_record = Some (if !primitive_flag then Some binder_name else None);
+      mind_entry_record = Some (if !primitive_flag then Some [|binder_name|] else None);
       mind_entry_finite = finite;
       mind_entry_inds = [mie_ind];
       mind_entry_private = None;