[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, 5 insertions, 15 deletions

diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
index 18955c2ba3..a6c577a878 100644
--- a/vernac/indschemes.ml
+++ b/vernac/indschemes.ml
@@ -98,19 +98,11 @@ let () =
 
 (* Util *)
 
-let define ~poly name sigma c t =
+let define ~poly name sigma c types =
   let f = declare_constant ~kind:Decls.(IsDefinition Scheme) in
   let univs = Evd.univ_entry ~poly sigma in
-  let kn = f ~name
-    (DefinitionEntry
-      { proof_entry_body = c;
-        proof_entry_secctx = None;
-        proof_entry_type = t;
-        proof_entry_universes = univs;
-        proof_entry_opaque = false;
-        proof_entry_inline_code = false;
-        proof_entry_feedback = None;
-      }) in
+  let entry = Declare.definition_entry ~univs ?types c in
+  let kn = f ~name (DefinitionEntry entry) in
   definition_message name;
   kn
 
@@ -411,8 +403,7 @@ let do_mutual_induction_scheme ?(force_mutual=false) lnamedepindsort =
   let declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 sigma (EConstr.of_constr decl) in
     let decltype = EConstr.to_constr sigma decltype in
-    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Evd.empty_side_effects) in
-    let cst = define ~poly fi sigma proof_output (Some decltype) in
+    let cst = define ~poly fi sigma decl (Some decltype) in
     GlobRef.ConstRef cst :: lrecref
   in
   let _ = List.fold_right2 declare listdecl lrecnames [] in
@@ -533,7 +524,6 @@ let do_combined_scheme name schemes =
       schemes
   in
   let sigma,body,typ = build_combined_scheme (Global.env ()) csts in
-  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Evd.empty_side_effects) in
   (* It is possible for the constants to have different universe
      polymorphism from each other, however that is only when the user
      manually defined at least one of them (as Scheme would pick the
@@ -541,7 +531,7 @@ let do_combined_scheme name schemes =
      some other polymorphism they can also manually define the
      combined scheme. *)
   let poly = Global.is_polymorphic (GlobRef.ConstRef (List.hd csts)) in
-  ignore (define ~poly name.v sigma proof_output (Some typ));
+  ignore (define ~poly name.v sigma body (Some typ));
   fixpoint_message None [name.v]
 
 (**********************************************************************)