[declare] Use entry constructor instead of low-level record.

Non-delayed entries can be done with the current constructor, delayed
ones will require more work.

1 files changed, 1 insertions, 9 deletions

diff --git a/vernac/record.ml b/vernac/record.ml
index 1bb8ddf5dc..11237f3873 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -340,15 +340,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
 		let projtyp =
                   it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
 	        try
-		  let entry = {
-                    proof_entry_body =
-                      Future.from_val ((proj, Univ.ContextSet.empty), Evd.empty_side_effects);
-                    proof_entry_secctx = None;
-                    proof_entry_type = Some projtyp;
-                    proof_entry_universes = ctx;
-                    proof_entry_opaque = false;
-                    proof_entry_inline_code = false;
-                    proof_entry_feedback = None } in
+                  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 =