[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, 24 insertions, 29 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]