[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.

5 files changed, 33 insertions, 76 deletions

diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 352b21a15a..92b7f2accf 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -164,7 +164,7 @@ let prepare_body { Vernacexpr.binders } rt =
   let fun_args,rt' = chop_rlambda_n n rt in
   (fun_args,rt')
 
-let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
+let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_map ref) interactive_proof old_princ_type sorts funs i proof_tac hook =
   (* First we get the type of the old graph principle *)
   let mutr_nparams = (Tactics.compute_elim_sig !evd (EConstr.of_constr old_princ_type)).Tactics.nparams in
   (*   let time1 = System.get_time ()  in *)
@@ -199,10 +199,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   (*    end; *)
 
   let open Proof_global in
-  let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+  let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
   match entries with
   | [entry] ->
-    name, entry, hook
+    entry, hook
   | _ ->
     CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
 
@@ -282,7 +282,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       register_with_sort Sorts.InProp;
       register_with_sort Sorts.InSet
   in
-  let id,entry,hook =
+  let entry, hook =
     build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
     proof_tac hook
   in
@@ -1219,9 +1219,21 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
         s::l_schemes -> s,l_schemes
       | _ -> CErrors.anomaly (Pp.str "")
   in
-  let _,const,_ =
+  let opaque =
+    let finfos =
+      match find_Function_infos (fst first_fun) with
+      | None -> raise Not_found
+      | Some finfos -> finfos
+    in
+    let open Proof_global in
+    match finfos.equation_lemma with
+    | None -> Transparent (* non recursive definition *)
+    | Some equation ->
+      if Declareops.is_opaque (Global.lookup_constant equation) then Opaque else Transparent
+  in
+  let entry, _hook =
     try
-      build_functional_principle evd false
+      build_functional_principle ~opaque evd false
         first_type
         (Array.of_list sorts)
         this_block_funs
@@ -1233,29 +1245,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
 
   in
   incr i;
-  let opacity =
-    let finfos =
-      match find_Function_infos (fst first_fun) with
-      | None -> raise Not_found
-      | Some finfos -> finfos
-    in
-    match finfos.equation_lemma with
-    | None -> false (* non recursive definition *)
-    | Some equation ->
-      Declareops.is_opaque (Global.lookup_constant equation)
-  in
-  let const = {const with Declare.proof_entry_opaque = opacity } in
   (* The others are just deduced *)
   if List.is_empty other_princ_types
-  then
-    [const]
+  then [entry]
   else
     let other_fun_princ_types =
       let funs = Array.map Constr.mkConstU this_block_funs in
       let sorts = Array.of_list sorts in
       List.map (Functional_principles_types.compute_new_princ_type_from_rel funs sorts) other_princ_types
     in
-    let first_princ_body,first_princ_type = Declare.(const.proof_entry_body, const.proof_entry_type) in
+    let first_princ_body,first_princ_type = Declare.(entry.proof_entry_body, entry.proof_entry_type) in
     let ctxt,fix = Term.decompose_lam_assum (fst(fst(Future.force first_princ_body))) in (* the principle has for forall ...., fix .*)
     let (idxs,_),(_,ta,_ as decl) = Constr.destFix fix in
     let other_result =
@@ -1282,7 +1281,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
              (* If we reach this point, the two principle are not mutually recursive
                 We fall back to the previous method
                 *)
-             let _,const,_ =
+             let entry, _hook =
                build_functional_principle
                  evd
                  false
@@ -1293,20 +1292,16 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : Evd.side_ef
                  (Functional_principles_proofs.prove_princ_for_struct evd false !i (Array.of_list (List.map fst funs)))
                  (fun _ _ -> ())
              in
-             const
+             entry
          with Found_type i ->
            let princ_body =
              Termops.it_mkLambda_or_LetIn (Constr.mkFix((idxs,i),decl)) ctxt
            in
-           { const with
-             Declare.proof_entry_body =
-               (Future.from_val ((princ_body, Univ.ContextSet.empty), Evd.empty_side_effects));
-             proof_entry_type = Some scheme_type
-           }
+           Declare.definition_entry ~types:scheme_type princ_body
       )
       other_fun_princ_types
     in
-    const::other_result
+    entry::other_result
 
 (* [derive_correctness funs graphs] create correctness and completeness
    lemmas for each function in [funs] w.r.t. [graphs]
diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml
index 1f973ace6f..54393dce00 100644
--- a/tactics/ind_tables.ml
+++ b/tactics/ind_tables.ml
@@ -124,17 +124,7 @@ let define internal role id c poly univs =
   let ctx = UState.minimize univs in
   let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in
   let univs = UState.univ_entry ~poly ctx in
-  let entry = {
-    Declare.proof_entry_body =
-      Future.from_val ((c,Univ.ContextSet.empty),
-                       Evd.empty_side_effects);
-    proof_entry_secctx = None;
-    proof_entry_type = None;
-    proof_entry_universes = univs;
-    proof_entry_opaque = false;
-    proof_entry_inline_code = false;
-    proof_entry_feedback = None;
-  } in
+  let entry = Declare.definition_entry ~univs c in
   let kn, eff = Declare.declare_private_constant ~role ~kind:Decls.(IsDefinition Scheme) ~name:id (Declare.DefinitionEntry entry) in
   let () = match internal with
     | InternalTacticRequest -> ()
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 9c8213ad8a..e3cffa8523 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -149,18 +149,8 @@ let declare_obligation prg obl body ty uctx =
       if get_shrink_obligations () && not poly then shrink_body body ty
       else ([], body, ty, [||])
     in
-    let body =
-      ((body, Univ.ContextSet.empty), Evd.empty_side_effects)
-    in
-    let ce =
-      { Declare.proof_entry_body = Future.from_val ~fix_exn:(fun x -> x) body
-      ; proof_entry_secctx = None
-      ; proof_entry_type = ty
-      ; proof_entry_universes = uctx
-      ; proof_entry_opaque = opaque
-      ; proof_entry_inline_code = false
-      ; proof_entry_feedback = None }
-    in
+    let ce = Declare.definition_entry ?types:ty ~opaque ~univs:uctx body in
+
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
       Declare.declare_constant ~name:obl.obl_name
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]
 
 (**********************************************************************)
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 =