Simplifying the declaration of constants bound to primitive projections.

We factorize code from declareInd.ml and inductiveops.ml which was
already existing in record.ml.

We keep expansion of local definitions in the type of fields of
primitive records while these are not expanded in the non-primitive
case. This is to be consistent with what Indtypes.compute_projections
is doing. See discussion at #11135.

We keep the unused code from inductiveops.ml for possible future use
though.

Include improvements contributed by Gaëtan Gilbert.

5 files changed, 87 insertions, 94 deletions

diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out
index e9c28faf1d..1dd89c9bcd 100644
--- a/test-suite/output/Projections.out
+++ b/test-suite/output/Projections.out
@@ -1,2 +1,17 @@
 fun S : store => S.(store_funcs)
      : store -> host_func
+a = 
+fun A : Type =>
+let B := A in fun (C : Type) (u : U A C) => (A, B, C, c _ _ u)
+     : forall A : Type,
+       let B := A in
+       forall C : Type, U A C -> Type * Type * Type * (B * A * C)
+
+Arguments a (_ _)%type_scope
+b = 
+fun A : Type => let B := A in fun (C : Type) (u : U A C) => b _ _ u
+     : forall A : Type,
+       let B := A in
+       forall (C : Type) (u : U A C), (A, B, C, c _ _ u) = (A, B, C, c _ _ u)
+
+Arguments b (_ _)%type_scope
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
index 14d63d39c4..83a581338f 100644
--- a/test-suite/output/Projections.v
+++ b/test-suite/output/Projections.v
@@ -10,3 +10,12 @@ Section store.
 End store.
 
 Check (fun (S:@store nat) => S.(store_funcs)).
+
+Module LocalDefUnfolding.
+
+Unset Printing Projections.
+Record U A (B:=A) C := {c:B*A*C;a:=(A,B,C,c);b:a=a}.
+Print a.
+Print b.
+
+End LocalDefUnfolding.
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml
index 2610f16d92..bbc5d493bf 100644
--- a/vernac/declareInd.ml
+++ b/vernac/declareInd.ml
@@ -93,38 +93,6 @@ let inPrim : (Projection.Repr.t * Constant.t) -> Libobject.obj =
 
 let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
 
-let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
-  let name = Label.to_id label in
-  let univs, u = match univs with
-    | Monomorphic_entry _ ->
-      (* Global constraints already defined through the inductive *)
-      Monomorphic_entry Univ.ContextSet.empty, Univ.Instance.empty
-    | Polymorphic_entry (nas, ctx) ->
-      Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx
-  in
-  let term = Vars.subst_instance_constr u term in
-  let types = Vars.subst_instance_constr u types in
-  let entry = Declare.definition_entry ~types ~univs term in
-  let cst = Declare.declare_constant ~name ~kind:Decls.(IsDefinition StructureComponent) (Declare.DefinitionEntry entry) in
-  let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in
-  declare_primitive_projection p cst
-
-let declare_projections univs mind =
-  let env = Global.env () in
-  let mib = Environ.lookup_mind mind env in
-  let open Declarations in
-  match mib.mind_record with
-  | PrimRecord info ->
-    let iter_ind i (_, labs, _, _) =
-      let ind = (mind, i) in
-      let projs = Inductiveops.compute_projections env ind in
-      CArray.iter2_i (declare_one_projection univs ind ~proj_npars:mib.mind_nparams) labs projs
-    in
-    let () = Array.iteri iter_ind info in
-    true
-  | FakeRecord -> false
-  | NotRecord -> false
-
 let feedback_axiom () = Feedback.(feedback AddedAxiom)
 
 let is_unsafe_typing_flags () =
@@ -146,7 +114,7 @@ let declare_mind mie =
   let (sp,kn as oname) = Lib.add_leaf id (inInductive { ind_names = names }) in
   if is_unsafe_typing_flags() then feedback_axiom ();
   let mind = Global.mind_of_delta_kn kn in
-  let isprim = declare_projections mie.mind_entry_universes mind in
+  let isprim = Inductive.is_primitive_record (Inductive.lookup_mind_specif (Global.env()) (mind,0)) in
   Impargs.declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
   oname, isprim
diff --git a/vernac/declareInd.mli b/vernac/declareInd.mli
index ae649634a5..05a1617329 100644
--- a/vernac/declareInd.mli
+++ b/vernac/declareInd.mli
@@ -30,3 +30,6 @@ type inductive_obj
 val objInductive : inductive_obj Libobject.Dyn.tag
 
 end
+
+val declare_primitive_projection :
+  Names.Projection.Repr.t -> Names.Constant.t -> unit
diff --git a/vernac/record.ml b/vernac/record.ml
index b9d450044b..0b6e8cd8c1 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -320,67 +320,65 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
   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 kn, term =
-              if is_local_assum decl && primitive then
-                let p = Projection.Repr.make indsp
-                    ~proj_npars:mib.mind_nparams
-                    ~proj_arg:i
-                    (Label.of_id fid)
-                in
-                (* Already defined by declare_mind silently *)
-                let kn = Projection.Repr.constant p in
-                Declare.definition_message fid;
-                kn, mkProj (Projection.make p false,mkRel 1)
-              else
-                let ccl = subst_projection fid subst ti in
-                let body = match decl with
-                  | LocalDef (_,ci,_) -> subst_projection fid subst ci
-                  | LocalAssum ({binder_relevance=rci},_) ->
-                    (* [ccl] is defined in context [params;x:rp] *)
-                    (* [ccl'] is defined in context [params;x:rp;x:rp] *)
-                    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 have no is *)
-                    mkCase (ci, p, mkRel 1, [|branch|])
-                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
-                try
-                  let entry = Declare.definition_entry ~univs:ctx ~types:projtyp proj in
-                  let kind = Decls.IsDefinition kind in
-                  let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in
-                  let constr_fip =
-                    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
-                      applist (mkConstU (kn,u),proj_args)
-                  in
-                  Declare.definition_message fid;
-                    kn, constr_fip
-                with Type_errors.TypeError (ctx,te) ->
-                  raise (NotDefinable (BadTypedProj (fid,ctx,te)))
-            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 ->
-              warning_or_error 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 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 have no is *)
+                     mkCase (ci, p, 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) when not primitive ->
+                   raise (NotDefinable (BadTypedProj (fid,ctx,te)))
+               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 ->
+               warning_or_error 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))
       (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls)
   in (kinds,sp_projs)