[record] Cleanup of data structure and functions [1/2]

In preparation for reworking the record declaration path to use the
common infrastructure, we perform some refactoring.

The current choices are far from definitive, as we will consolidate
the data types more as we move along with the work here.

3 files changed, 243 insertions, 187 deletions

diff --git a/vernac/record.ml b/vernac/record.ml
index 2c56604d8f..ebd83bb6d2 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -11,24 +11,17 @@
 open Pp
 open CErrors
 open Term
-open Sorts
 open Util
 open Names
-open Nameops
 open Constr
 open Context
-open Vars
 open Environ
 open Declarations
 open Entries
-open Declare
-open Constrintern
 open Type_errors
 open Constrexpr
 open Constrexpr_ops
-open Goptions
 open Context.Rel.Declaration
-open Libobject
 
 module RelDecl = Context.Rel.Declaration
 
@@ -37,6 +30,7 @@ module RelDecl = Context.Rel.Declaration
 (** Flag governing use of primitive projections. Disabled by default. *)
 let primitive_flag = ref false
 let () =
+  let open Goptions in
   declare_bool_option
     { optdepr  = false;
       optkey   = ["Primitive";"Projections"];
@@ -45,6 +39,7 @@ let () =
 
 let typeclasses_strict = ref false
 let () =
+  let open Goptions in
   declare_bool_option
     { optdepr  = false;
       optkey   = ["Typeclasses";"Strict";"Resolution"];
@@ -53,6 +48,7 @@ let () =
 
 let typeclasses_unique = ref false
 let () =
+  let open Goptions in
   declare_bool_option
     { optdepr  = false;
       optkey   = ["Typeclasses";"Unique";"Instances"];
@@ -81,7 +77,8 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
          let impls_env =
            match i with
            | Anonymous -> impls_env
-           | Name id -> Id.Map.add id (compute_internalization_data env sigma id Constrintern.Method t impl) impls_env
+           | Name id ->
+             Id.Map.add id (Constrintern.compute_internalization_data env sigma id Constrintern.Method t impl) impls_env
          in
          let d = match b with
            | None -> LocalAssum (make_annot i r,t)
@@ -106,7 +103,7 @@ let compute_constructor_level evars env l =
     let univ =
       if is_local_assum d then
         let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
-          Univ.sup (univ_of_sort s) univ
+          Univ.sup (Sorts.univ_of_sort s) univ
       else univ
     in (EConstr.push_rel d env, univ))
     l (env, Univ.Universe.sprop)
@@ -116,68 +113,83 @@ let check_anonymous_type ind =
   | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true
   | _ -> false
 
-let typecheck_params_and_fields def poly pl ps records =
+let error_parameters_must_be_named bk {CAst.loc; v=name} =
+  match bk, name with
+  | Default _, Anonymous ->
+    CErrors.user_err ?loc ~hdr:"record" (str "Record parameters must be named")
+  | _ -> ()
+
+let check_parameters_must_be_named = function
+  | CLocalDef (b, _, _) ->
+    error_parameters_must_be_named default_binder_kind b
+  | CLocalAssum (ls, bk, ce) ->
+    List.iter (error_parameters_must_be_named bk) ls
+  | CLocalPattern {CAst.loc} ->
+    Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")
+
+module DataI = struct
+  type t =
+    { name : Id.t
+    ; arity : Constrexpr.constr_expr option
+    ; nots : Vernacexpr.decl_notation list list
+    ; fs : Vernacexpr.local_decl_expr list
+    }
+end
+
+let build_type_telescope newps env0 (sigma, template) { DataI.arity; _ } = match arity with
+  | None ->
+    let uvarkind = Evd.univ_flexible_alg in
+    let sigma, s = Evd.new_sort_variable uvarkind sigma in
+    (sigma, template), (EConstr.mkSort s, s)
+  | Some t ->
+    let env = EConstr.push_rel_context newps env0 in
+    let poly =
+      match t with
+      | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false in
+    let impls = Constrintern.empty_internalization_env in
+    let sigma, s = Constrintern.interp_type_evars ~program_mode:false env sigma ~impls t in
+    let sred = Reductionops.whd_allnolet env sigma s in
+    (match EConstr.kind sigma sred with
+     | Sort s' ->
+       let s' = EConstr.ESorts.kind sigma s' in
+       (if poly then
+          match Evd.is_sort_variable sigma s' with
+          | Some l ->
+            let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in
+            (sigma, template), (s, s')
+          | None ->
+            (sigma, false), (s, s')
+        else (sigma, false), (s, s'))
+     | _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
+
+(* ps = parameter list *)
+let typecheck_params_and_fields def poly pl ps (records : DataI.t list) =
   let env0 = Global.env () in
   (* Special case elaboration for template-polymorphic inductives,
      lower bound on introduced universes is Prop so that we do not miss
      any Set <= i constraint for universes that might actually be instantiated with Prop. *)
   let is_template =
-    List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
+    List.exists (fun { DataI.arity; _} -> Option.cata check_anonymous_type true arity) records in
   let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
-  let sigma, decl = interp_univ_decl_opt env0 pl in
-  let () =
-    let error bk {CAst.loc; v=name} =
-      match bk, name with
-      | Default _, Anonymous ->
-        user_err ?loc ~hdr:"record" (str "Record parameters must be named")
-      | _ -> ()
-    in
-      List.iter
-        (function CLocalDef (b, _, _) -> error default_binder_kind b
-           | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
-           | CLocalPattern {CAst.loc} ->
-              Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps
-  in
-  let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars ~program_mode:false env0 sigma ps in
-  let fold (sigma, template) (_, t, _, _) = match t with
-    | Some t ->
-       let env = EConstr.push_rel_context newps env0 in
-       let poly =
-         match t with
-         | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true | _ -> false in
-       let sigma, s = interp_type_evars ~program_mode:false env sigma ~impls:empty_internalization_env t in
-       let sred = Reductionops.whd_allnolet env sigma s in
-         (match EConstr.kind sigma sred with
-         | Sort s' ->
-            let s' = EConstr.ESorts.kind sigma s' in
-            (if poly then
-               match Evd.is_sort_variable sigma s' with
-               | Some l ->
-                 let sigma = Evd.make_flexible_variable sigma ~algebraic:true l in
-                 (sigma, template), (s, s')
-               | None ->
-                 (sigma, false), (s, s')
-             else (sigma, false), (s, s'))
-         | _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
-    | None ->
-      let uvarkind = Evd.univ_flexible_alg in
-      let sigma, s = Evd.new_sort_variable uvarkind sigma in
-      (sigma, template), (EConstr.mkSort s, s)
-  in
-  let (sigma, template), typs = List.fold_left_map fold (sigma, true) records in
+  let sigma, decl = Constrintern.interp_univ_decl_opt env0 pl in
+  let () = List.iter check_parameters_must_be_named ps in
+  let sigma, (impls_env, ((env1,newps), imps)) =
+    Constrintern.interp_context_evars ~program_mode:false env0 sigma ps in
+  let (sigma, template), typs =
+    List.fold_left_map (build_type_telescope newps env0) (sigma, true) records in
   let arities = List.map (fun (typ, _) -> EConstr.it_mkProd_or_LetIn typ newps) typs in
   let relevances = List.map (fun (_,s) -> Sorts.relevance_of_sort s) typs in
-  let fold accu (id, _, _, _) arity r =
-    EConstr.push_rel (LocalAssum (make_annot (Name id) r,arity)) accu in
+  let fold accu { DataI.name; _ } arity r =
+    EConstr.push_rel (LocalAssum (make_annot (Name name) r,arity)) accu in
   let env_ar = EConstr.push_rel_context newps (List.fold_left3 fold env0 records arities relevances) in
   let impls_env =
-    let ids = List.map (fun (id, _, _, _) -> id) records in
+    let ids = List.map (fun { DataI.name; _ } -> name) records in
     let imps = List.map (fun _ -> imps) arities in
-    compute_internalization_env env0 sigma ~impls:impls_env Inductive ids arities imps
+    Constrintern.compute_internalization_env env0 sigma ~impls:impls_env Constrintern.Inductive ids arities imps
   in
   let ninds = List.length arities in
   let nparams = List.length newps in
-  let fold sigma (_, _, nots, fs) arity =
+  let fold sigma { DataI.nots; fs; _ } arity =
     interp_fields_evars env_ar sigma ~ninds ~nparams impls_env nots fs
   in
   let (sigma, data) = List.fold_left2_map fold sigma records arities in
@@ -299,20 +311,92 @@ type projection_flags = {
 }
 
 (* We build projections *)
-let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields =
+
+(* TODO: refactor the declaration part here; this requires some
+   surgery as Evarutil.finalize is called too early in the path *)
+let build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs
+    (nfi,i,kinds,sp_projs,subst) flags decl impls =
+  let fi = RelDecl.get_name decl in
+  let ti = RelDecl.get_type decl in
+  let (sp_projs,i,subst) =
+    match fi with
+    | Anonymous ->
+      (None::sp_projs,i,NoProjection fi::subst)
+    | Name fid ->
+      try
+        let ccl = subst_projection fid subst ti in
+        let body, p_opt = match decl with
+          | LocalDef (_,ci,_) -> subst_projection fid subst ci, None
+          | LocalAssum ({binder_relevance=rci},_) ->
+            (* [ccl] is defined in context [params;x:rp] *)
+            (* [ccl'] is defined in context [params;x:rp;x:rp] *)
+            if primitive then
+              let p = Projection.Repr.make indsp
+                  ~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in
+              mkProj (Projection.make p true, mkRel 1), Some p
+            else
+              let ccl' = liftn 1 2 ccl in
+              let p = mkLambda (x, lift 1 rp, ccl') in
+              let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
+              let ci = Inductiveops.make_case_info env indsp rci LetStyle in
+              (* Record projections are always NoInvert because
+                        they're at constant relevance *)
+              mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None
+        in
+        let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
+        let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
+        let entry = Declare.definition_entry ~univs ~types:projtyp proj in
+        let kind = Decls.IsDefinition kind in
+        let kn =
+          try Declare.declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry)
+          with Type_errors.TypeError (ctx,te) as exn when not primitive ->
+            let _, info = Exninfo.capture exn in
+            Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info)
+        in
+        Declare.definition_message fid;
+        let term = match p_opt with
+          | Some p ->
+            let _ = DeclareInd.declare_primitive_projection p kn in
+            mkProj (Projection.make p false,mkRel 1)
+          | None ->
+            let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
+            match decl with
+            | LocalDef (_,ci,_) when primitive -> body
+            | _ -> applist (mkConstU (kn,uinstance),proj_args)
+        in
+        let refi = GlobRef.ConstRef kn in
+        Impargs.maybe_declare_manual_implicits false refi impls;
+        if flags.pf_subclass then begin
+          let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
+          ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
+        end;
+        let i = if is_local_assum decl then i+1 else i in
+        (Some kn::sp_projs, i, Projection term::subst)
+      with NotDefinable why as exn ->
+        let _, info = Exninfo.capture exn in
+        warning_or_error ~info flags.pf_subclass indsp why;
+        (None::sp_projs,i,NoProjection fi::subst)
+  in
+  (nfi - 1, i,
+   { Recordops.pk_name = fi
+   ; pk_true_proj = is_local_assum decl
+   ; pk_canonical = flags.pf_canonical } :: kinds
+  , sp_projs, subst)
+
+let declare_projections indsp univs ?(kind=Decls.StructureComponent) binder_name flags fieldimpls fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
   let poly = Declareops.inductive_is_polymorphic mib in
-  let u = match ctx with
+  let uinstance = match univs with
     | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
     | Monomorphic_entry ctx -> Univ.Instance.empty
   in
-  let paramdecls = Inductive.inductive_paramdecls (mib, u) in
-  let r = mkIndU (indsp,u) in
+  let paramdecls = Inductive.inductive_paramdecls (mib, uinstance) in
+  let r = mkIndU (indsp,uinstance) in
   let rp = applist (r, Context.Rel.to_extended_list mkRel 0 paramdecls) in
   let paramargs = Context.Rel.to_extended_list mkRel 1 paramdecls in (*def in [[params;x:rp]]*)
   let x = make_annot (Name binder_name) mip.mind_relevance in
-  let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in
+  let fields = instantiate_possibly_recursive_type (fst indsp) uinstance mib.mind_ntypes paramdecls fields in
   let lifted_fields = Termops.lift_rel_context 1 fields in
   let primitive =
     match mib.mind_record with
@@ -321,69 +405,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
   in
   let (_,_,kinds,sp_projs,_) =
     List.fold_left3
-      (fun (nfi,i,kinds,sp_projs,subst) flags decl impls ->
-         let fi = RelDecl.get_name decl in
-         let ti = RelDecl.get_type decl in
-         let (sp_projs,i,subst) =
-           match fi with
-           | Anonymous ->
-             (None::sp_projs,i,NoProjection fi::subst)
-           | Name fid ->
-             try
-               let ccl = subst_projection fid subst ti in
-               let body, p_opt = match decl with
-                 | LocalDef (_,ci,_) -> subst_projection fid subst ci, None
-                 | LocalAssum ({binder_relevance=rci},_) ->
-                   (* [ccl] is defined in context [params;x:rp] *)
-                   (* [ccl'] is defined in context [params;x:rp;x:rp] *)
-                   if primitive then
-                     let p = Projection.Repr.make indsp
-                         ~proj_npars:mib.mind_nparams ~proj_arg:i (Label.of_id fid) in
-                     mkProj (Projection.make p true, mkRel 1), Some p
-                   else
-                     let ccl' = liftn 1 2 ccl in
-                     let p = mkLambda (x, lift 1 rp, ccl') in
-                     let branch = it_mkLambda_or_LetIn (mkRel nfi) lifted_fields in
-                     let ci = Inductiveops.make_case_info env indsp rci LetStyle in
-                     (* Record projections are always NoInvert because
-                        they're at constant relevance *)
-                     mkCase (ci, p, NoInvert, mkRel 1, [|branch|]), None
-               in
-               let proj = it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
-               let projtyp = it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
-               let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in
-               let kind = Decls.IsDefinition kind in
-               let kn =
-                 try declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry)
-                 with Type_errors.TypeError (ctx,te) as exn when not primitive ->
-                   let _, info = Exninfo.capture exn in
-                   Exninfo.iraise (NotDefinable (BadTypedProj (fid,ctx,te)),info)
-               in
-               Declare.definition_message fid;
-               let term = match p_opt with
-                 | Some p ->
-                   let _ = DeclareInd.declare_primitive_projection p kn in
-                   mkProj (Projection.make p false,mkRel 1)
-                 | None ->
-                   let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
-                   match decl with
-                   | LocalDef (_,ci,_) when primitive -> body
-                   | _ -> applist (mkConstU (kn,u),proj_args)
-               in
-               let refi = GlobRef.ConstRef kn in
-               Impargs.maybe_declare_manual_implicits false refi impls;
-               if flags.pf_subclass then begin
-                 let cl = ComCoercion.class_of_global (GlobRef.IndRef indsp) in
-                 ComCoercion.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
-               end;
-               let i = if is_local_assum decl then i+1 else i in
-               (Some kn::sp_projs, i, Projection term::subst)
-             with NotDefinable why as exn ->
-               let _, info = Exninfo.capture exn in
-               warning_or_error ~info flags.pf_subclass indsp why;
-               (None::sp_projs,i,NoProjection fi::subst)
-         in
-         (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst))
+      (build_proj env mib indsp primitive x rp lifted_fields ~poly paramdecls paramargs ~uinstance ~kind ~univs)
       (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)
 
@@ -402,7 +424,8 @@ let discharge_structure (_, x) = Some x
 
 let rebuild_structure s = Recordops.rebuild_structure (Global.env()) s
 
-let inStruc : Recordops.struc_typ -> obj =
+let inStruc : Recordops.struc_typ -> Libobject.obj =
+  let open Libobject in
   declare_object {(default_object "STRUCTURE") with
     cache_function = cache_structure;
     load_function = load_structure;
@@ -414,7 +437,20 @@ let inStruc : Recordops.struc_typ -> obj =
 let declare_structure_entry o =
   Lib.add_anonymous_leaf (inStruc o)
 
-let declare_structure ~cumulative finite ubinders univs paramimpls params template ?(kind=Decls.StructureComponent) ?name record_data =
+module Data = struct
+  type t =
+  { id : Id.t
+  ; idbuild : Id.t
+  ; min_univ : Univ.Universe.t
+  ; arity : Constr.t
+  ; fieldimpls : Impargs.manual_implicits list
+  ; fields : Constr.rel_context
+  ; is_coercion : bool
+  ; coers : projection_flags list
+  }
+end
+
+let declare_structure ~cumulative finite ubinders ~univs paramimpls params template ?(kind=Decls.StructureComponent) ?name (record_data : Data.t list) =
   let nparams = List.length params in
   let poly, ctx =
     match univs with
@@ -426,14 +462,14 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
   let binder_name =
     match name with
     | None ->
-      let map (id, _, _, _, _, _, _, _) =
+      let map { Data.id; _ } =
         Id.of_string (Unicode.lowercase_first_char (Id.to_string id))
       in
       Array.map_of_list map record_data
     | Some n -> n
   in
   let ntypes = List.length record_data in
-  let mk_block i (id, idbuild, min_univ, arity, _, fields, _, _) =
+  let mk_block i { Data.id; idbuild; min_univ; arity; fields; _ } =
     let nfields = List.length fields in
     let args = Context.Rel.to_extended_list mkRel nfields params in
     let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
@@ -444,7 +480,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
       mind_entry_lc = [type_constructor] }
   in
   let blocks = List.mapi mk_block record_data in
-  let check_template (id, _, min_univ, _, _, fields, _, _) =
+  let check_template { Data.id; min_univ; fields; _ } =
       let template_candidate () =
         (* we use some dummy values for the arities in the rel_context
            as univs_of_constr doesn't care about localassums and
@@ -479,7 +515,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
   let template = List.for_all check_template record_data in
   let primitive =
     !primitive_flag &&
-    List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
+    List.for_all (fun { Data.fields; _ } -> List.exists is_local_assum fields) record_data
   in
   let mie =
     { mind_entry_params = params;
@@ -496,12 +532,12 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
   let kn = DeclareInd.declare_mutual_inductive_with_eliminations mie ubinders impls
       ~primitive_expected:!primitive_flag
   in
-  let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) =
+  let map i { Data.fieldimpls; fields; is_coercion; coers } =
     let rsp = (kn, i) in (* This is ind path of idstruc *)
     let cstr = (rsp, 1) in
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
     let build = GlobRef.ConstructRef cstr in
-    let () = if is_coe then ComCoercion.try_add_new_coercion build ~local:false ~poly in
+    let () = if is_coercion then ComCoercion.try_add_new_coercion build ~local:false ~poly in
     let npars = Inductiveops.inductive_nparams (Global.env()) rsp in
     let struc = {
       Recordops.s_CONST = cstr;
@@ -519,7 +555,7 @@ let implicits_of_context ctx =
   List.map (fun name -> CAst.make (Some (name,true)))
     (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
-let declare_class def cumulative ubinders univs id idbuild paramimpls params univ arity
+let declare_class def cumulative ubinders univs id idbuild paramimpls params min_univ arity
     template fieldimpls fields ?(kind=Decls.StructureComponent) coers =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
@@ -529,15 +565,15 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
   let binder_name = Namegen.next_ident_away id (Termops.vars_of_env (Global.env())) in
   let data =
     match fields with
-    | [LocalAssum ({binder_name=Name proj_name} as binder, field)
-      | LocalDef ({binder_name=Name proj_name} as binder, _, field)] when def ->
+    | [ LocalAssum ({binder_name=Name proj_name} as binder, field)
+      | LocalDef ({binder_name=Name proj_name} as binder, _, field) ] when def ->
       let binder = {binder with binder_name=Name binder_name} in
       let class_body = it_mkLambda_or_LetIn field params in
       let class_type = it_mkProd_or_LetIn arity params in
       let class_entry =
         Declare.definition_entry ~types:class_type ~univs class_body in
       let cst = Declare.declare_constant ~name:id
-        (DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition)
+        (Declare.DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition)
       in
       let inst, univs = match univs with
         | Polymorphic_entry (_, uctx) -> Univ.UContext.instance uctx, univs
@@ -552,7 +588,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
         it_mkLambda_or_LetIn (mkLambda (binder, inst_type, mkRel 1)) params in
       let proj_entry = Declare.definition_entry ~types:proj_type ~univs proj_body in
       let proj_cst = Declare.declare_constant ~name:proj_name
-        (DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition)
+        (Declare.DefinitionEntry proj_entry) ~kind:Decls.(IsDefinition Definition)
       in
       let cref = GlobRef.ConstRef cst in
       Impargs.declare_manual_implicits false cref paramimpls;
@@ -566,10 +602,18 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params uni
       } in
       [cref, [m]]
     | _ ->
-      let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false,
-                         List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
-      let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls
-        params template ~kind:Decls.Method ~name:[|binder_name|] record_data
+      let record_data =
+        { Data.id
+        ; idbuild
+        ; min_univ
+        ; arity
+        ; fieldimpls
+        ; fields
+        ; is_coercion = false
+        ; coers = List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields
+        } in
+      let inds = declare_structure ~cumulative Declarations.BiFinite ubinders ~univs paramimpls
+        params template ~kind:Decls.Method ~name:[|binder_name|] [record_data]
       in
       let map ind =
         let map decl b y = {
@@ -667,14 +711,34 @@ let declare_existing_class g =
 
 open Vernacexpr
 
+module Ast = struct
+  type t =
+    { name : Names.lident
+    ; is_coercion : coercion_flag
+    ; binders: local_binder_expr list
+    ; cfs : (local_decl_expr * record_field_attr) list
+    ; idbuild : Id.t
+    ; sort : constr_expr option
+    }
+
+  let to_idata { name; is_coercion; cfs; idbuild; sort } =
+    let fs = List.map fst cfs in
+    { DataI.name = name.CAst.v
+    ; arity = sort
+    ; nots = List.map (fun (_, { rf_notation }) -> rf_notation) cfs
+    ; fs
+    }
+
+end
+
 let check_unique_names records =
   let extract_name acc (rf_decl, _) = match rf_decl with
       Vernacexpr.AssumExpr({CAst.v=Name id},_,_) -> id::acc
     | Vernacexpr.DefExpr ({CAst.v=Name id},_,_,_) -> id::acc
     | _ -> acc in
   let allnames =
-    List.fold_left (fun acc (_, id, _, cfs, _, _) ->
-      id.CAst.v :: (List.fold_left extract_name acc cfs)) [] records
+    List.fold_left (fun acc { Ast.name; cfs; _ } ->
+      name.CAst.v :: (List.fold_left extract_name acc cfs)) [] records
   in
   match List.duplicates Id.equal allnames with
   | [] -> ()
@@ -682,19 +746,15 @@ let check_unique_names records =
 
 let check_priorities kind records =
   let isnot_class = match kind with Class false -> false | _ -> true in
-  let has_priority (_, _, _, cfs, _, _) =
+  let has_priority { Ast.cfs; _ } =
     List.exists (fun (_, { rf_priority }) -> not (Option.is_empty rf_priority)) cfs
   in
   if isnot_class && List.exists has_priority records then
     user_err Pp.(str "Priorities only allowed for type class substructures")
 
 let extract_record_data records =
-  let map (is_coe, id, _, cfs, idbuild, s) =
-    let fs = List.map fst cfs in
-    id.CAst.v, s, List.map (fun (_, { rf_notation }) -> rf_notation) cfs, fs
-  in
-  let data = List.map map records in
-  let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in
+  let data = List.map Ast.to_idata records in
+  let pss = List.map (fun { Ast.binders; _ } -> binders) records in
   let ps = match pss with
   | [] -> CErrors.anomaly (str "Empty record block")
   | ps :: rem ->
@@ -711,40 +771,44 @@ let extract_record_data records =
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions
    or subinstances. *)
-let definition_structure udecl kind ~template ~cumulative ~poly finite records =
+let definition_structure udecl kind ~template ~cumulative ~poly finite (records : Ast.t list) =
   let () = check_unique_names records in
   let () = check_priorities kind records in
   let ps, data = extract_record_data records in
   let ubinders, univs, auto_template, params, implpars, data =
+    (* In theory we should be able to use
+       [Notation.with_notation_protection], due to the call to
+       Metasyntax.set_notation_for_interpretation, however something
+       is messing state beyond that.
+    *)
     Vernacstate.System.protect (fun () ->
       typecheck_params_and_fields (kind = Class true) poly udecl ps data) () in
   let template = template, auto_template in
   match kind with
   | Class def ->
-    let (_, id, _, cfs, idbuild, _), (univ, arity, implfs, fields) = match records, data with
+    let { Ast.name; cfs; idbuild; _ }, (univ, arity, implfs, fields) = match records, data with
     | [r], [d] -> r, d
     | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
     in
-    let coers = List.map (fun (_, { rf_subclass=coe; rf_priority=pri }) ->
-        match coe with
-        | Vernacexpr.BackInstance -> Some {hint_priority = pri ; hint_pattern = None}
+    let coers = List.map (fun (_, { rf_subclass; rf_priority }) ->
+        match rf_subclass with
+        | Vernacexpr.BackInstance -> Some {hint_priority = rf_priority; hint_pattern = None}
         | Vernacexpr.NoInstance -> None)
-        cfs
-    in
-    declare_class def cumulative ubinders univs id.CAst.v idbuild
+        cfs in
+    declare_class def cumulative ubinders univs name.CAst.v idbuild
       implpars params univ arity template implfs fields coers
   | _ ->
     let map impls = implpars @ [CAst.make None] @ impls in
     let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in
-    let map (univ, arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
-      let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
+    let map (min_univ, arity, fieldimpls, fields) { Ast.name; is_coercion; cfs; idbuild; _ } =
+      let coers = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
           { pf_subclass =
               (match rf_subclass with Vernacexpr.BackInstance -> true | Vernacexpr.NoInstance -> false);
             pf_canonical = rf_canonical })
           cfs
       in
-      id.CAst.v, idbuild, univ, arity, implfs, fields, is_coe, coe
+      { Data.id = name.CAst.v; idbuild; min_univ; arity; fieldimpls; fields; is_coercion; coers }
     in
     let data = List.map2 map data records in
-    let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in
+    let inds = declare_structure ~cumulative finite ubinders ~univs implpars params template data in
     List.map (fun ind -> GlobRef.IndRef ind) inds
diff --git a/vernac/record.mli b/vernac/record.mli
index 38a622977a..c3b84540f0 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -14,20 +14,16 @@ open Constrexpr
 
 val primitive_flag : bool ref
 
-type projection_flags = {
-  pf_subclass: bool;
-  pf_canonical: bool;
-}
-
-val declare_projections :
-  inductive ->
-  Entries.universes_entry ->
-  ?kind:Decls.definition_object_kind ->
-  Id.t ->
-  projection_flags list ->
-  Impargs.manual_implicits list ->
-  Constr.rel_context ->
-    Recordops.proj_kind list * Constant.t option list
+module Ast : sig
+  type t =
+    { name : Names.lident
+    ; is_coercion : coercion_flag
+    ; binders: local_binder_expr list
+    ; cfs : (local_decl_expr * record_field_attr) list
+    ; idbuild : Id.t
+    ; sort : constr_expr option
+    }
+end
 
 val definition_structure
   :  universe_decl_expr option
@@ -36,11 +32,7 @@ val definition_structure
   -> cumulative:bool
   -> poly:bool
   -> Declarations.recursivity_kind
-  -> (coercion_flag *
-      Names.lident *
-      local_binder_expr list *
-      (local_decl_expr * record_field_attr) list *
-      Id.t * constr_expr option) list
+  -> Ast.t list
   -> GlobRef.t list
 
 val declare_existing_class : GlobRef.t -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 824bf35b1d..6a09250627 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -715,16 +715,16 @@ let should_treat_as_uniform () =
   else ComInductive.NonUniformParameters
 
 let vernac_record ~template udecl ~cumulative k ~poly finite records =
-  let map ((coe, id), binders, sort, nameopt, cfs) =
-    let const = match nameopt with
-    | None -> Nameops.add_prefix "Build_" id.v
+  let map ((is_coercion, name), binders, sort, nameopt, cfs) =
+    let idbuild = match nameopt with
+    | None -> Nameops.add_prefix "Build_" name.v
     | Some lid ->
       let () = Dumpglob.dump_definition lid false "constr" in
       lid.v
     in
     let () =
       if Dumpglob.dump () then
-        let () = Dumpglob.dump_definition id false "rec" in
+        let () = Dumpglob.dump_definition name false "rec" in
         let iter (x, _) = match x with
         | Vernacexpr.(AssumExpr ({loc;v=Name id}, _, _) | DefExpr ({loc;v=Name id}, _, _, _)) ->
           Dumpglob.dump_definition (make ?loc id) false "proj"
@@ -732,7 +732,7 @@ let vernac_record ~template udecl ~cumulative k ~poly finite records =
         in
         List.iter iter cfs
     in
-    coe, id, binders, cfs, const, sort
+    Record.Ast.{ name; is_coercion; binders; cfs; idbuild; sort }
   in
   let records = List.map map records in
   ignore(Record.definition_structure ~template udecl k ~cumulative ~poly finite records)