[declare] Return list of declared global in Proof.save

This is needed in rewriter as to avoid hack; indeed it makes sense to
propagate this information to the callers of save.

7 files changed, 31 insertions, 21 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index afe89aef6e..2151ad7873 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -861,7 +861,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   let lemma, _ =
     Declare.Proof.by (Proofview.V82.tactic prove_replacement) lemma
   in
-  let () =
+  let (_ : _ list) =
     Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
   in
   evd
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 0cd5df12f7..167cf37026 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -1524,7 +1524,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
           let lemma =
             fst @@ Declare.Proof.by (Proofview.V82.tactic (proving_tac i)) lemma
           in
-          let () =
+          let (_ : GlobRef.t list) =
             Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
               ~idopt:None
           in
@@ -1596,7 +1596,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list)
                        (proving_tac i)))
                  lemma)
           in
-          let () =
+          let (_ : _ list) =
             Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent
               ~idopt:None
           in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 92eb85ffd8..884792cc15 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -58,7 +58,10 @@ let declare_fun name kind ?univs value =
     (Declare.declare_constant ~name ~kind (Declare.DefinitionEntry ce))
 
 let defined lemma =
-  Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+  let (_ : _ list) =
+    Declare.Proof.save ~proof:lemma ~opaque:Vernacexpr.Transparent ~idopt:None
+  in
+  ()
 
 let def_of_const t =
   match Constr.kind t with
@@ -1489,7 +1492,10 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name
                      [Hints.Hint_db.empty TransparentState.empty false] ]))
     in
     let lemma = build_proof env (Evd.from_env env) start_tac end_tac in
-    Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
+    let (_ : _ list) =
+      Declare.Proof.save ~proof:lemma ~opaque:opacity ~idopt:None
+    in
+    ()
   in
   let info = Declare.Info.make ~hook:(Declare.Hook.make hook) () in
   let cinfo = Declare.CInfo.make ~name:na ~typ:gls_type () in
diff --git a/vernac/declare.ml b/vernac/declare.ml
index 705a136a67..6326a22e83 100644
--- a/vernac/declare.ml
+++ b/vernac/declare.ml
@@ -877,7 +877,8 @@ let declare_obligation prg obl ~uctx ~types ~body =
   let body = prg.prg_reduce body in
   let types = Option.map prg.prg_reduce types in
   match obl.obl_status with
-  | _, Evar_kinds.Expand -> (false, {obl with obl_body = Some (TermObl body)})
+  | _, Evar_kinds.Expand ->
+    (false, {obl with obl_body = Some (TermObl body)}, [])
   | force, Evar_kinds.Define opaque ->
     let opaque = (not force) && opaque in
     let poly = prg.prg_info.Info.poly in
@@ -907,7 +908,7 @@ let declare_obligation prg obl ~uctx ~types ~body =
                 (mkApp (mkConst constant, args))
                 ctx))
     in
-    (true, {obl with obl_body = body})
+    (true, {obl with obl_body = body}, [GlobRef.ConstRef constant])
 
 (* Updating the obligation meta-info on close *)
 
@@ -1256,7 +1257,7 @@ let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} =
   let obl = {obl with obl_status = (false, status)} in
   let poly = prg.prg_info.Info.poly in
   let uctx = if poly then uctx else UState.union prg.prg_uctx uctx in
-  let defined, obl = declare_obligation prg obl ~body ~types:ty ~uctx in
+  let defined, obl, cst = declare_obligation prg obl ~body ~types:ty ~uctx in
   let prg_ctx =
     if poly then
       (* Polymorphic *)
@@ -1273,7 +1274,8 @@ let obligation_terminator ~entry ~uctx ~oinfo:{name; num; auto} =
       UState.from_env (Global.env ())
     else uctx
   in
-  update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto
+  update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto;
+  cst
 
 (* Similar to the terminator but for the admitted path; this assumes
    the admitted constant was already declared.
@@ -2008,8 +2010,8 @@ let finish_derived ~f ~name ~entries =
   (* The same is done in the body of the proof. *)
   let lemma_def = Internal.map_entry_body lemma_def ~f:(fun ((b,ctx),fx) -> (substf b, ctx), fx) in
   let lemma_def = DefinitionEntry lemma_def in
-  let _ : Names.Constant.t = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
-  ()
+  let ct = declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
+  [GlobRef.ConstRef ct]
 
 let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
 
@@ -2028,7 +2030,8 @@ let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
         sigma, cst) sigma0
       types proof_obj.entries
   in
-  hook recobls sigma
+  hook recobls sigma;
+  List.map (fun cst -> GlobRef.ConstRef cst) recobls
 
 let check_single_entry { entries; uctx } label =
   match entries with
@@ -2041,9 +2044,7 @@ let finalize_proof proof_obj proof_info =
   match CEphemeron.default proof_info.Proof_info.proof_ending Regular with
   | Regular ->
     let entry, uctx = check_single_entry proof_obj "Proof.save" in
-    let _ : GlobRef.t list =
-      MutualEntry.declare_mutdef ~entry ~uctx ~pinfo:proof_info in
-    ()
+    MutualEntry.declare_mutdef ~entry ~uctx ~pinfo:proof_info
   | End_obligation oinfo ->
     let entry, uctx = check_single_entry proof_obj "Obligation.save" in
     Obls_.obligation_terminator ~entry ~uctx ~oinfo
@@ -2286,7 +2287,7 @@ and solve_obligation_by_tac prg obls i tac =
         | None -> None
         | Some (t, ty, uctx) ->
           let prg = ProgramDecl.Internal.set_uctx ~uctx prg in
-          let def, obl' = declare_obligation prg obl ~body:t ~types:ty ~uctx in
+          let def, obl', _cst = declare_obligation prg obl ~body:t ~types:ty ~uctx in
           obls.(i) <- obl';
           if def && not poly then (
             (* Declare the term constraints with the first obligation only *)
diff --git a/vernac/declare.mli b/vernac/declare.mli
index dc1c28edce..4891e66803 100644
--- a/vernac/declare.mli
+++ b/vernac/declare.mli
@@ -201,7 +201,7 @@ module Proof : sig
     : proof:t
     -> opaque:Vernacexpr.opacity_flag
     -> idopt:Names.lident option
-    -> unit
+    -> GlobRef.t list
 
   (** Admit a proof *)
   val save_admitted : proof:t -> unit
@@ -295,7 +295,7 @@ module Proof : sig
     : proof:proof_object
     -> pinfo:Proof_info.t
     -> idopt:Names.lident option
-    -> unit
+    -> GlobRef.t list
 
   (** Used by the STM only to store info, should go away *)
   val get_po_name : proof_object -> Id.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 1a276ecbad..cc582727e3 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -613,13 +613,14 @@ let vernac_end_proof ~lemma = let open Vernacexpr in function
   | Admitted ->
     Declare.Proof.save_admitted ~proof:lemma
   | Proved (opaque,idopt) ->
-    Declare.Proof.save ~proof:lemma ~opaque ~idopt
+    let _ : Names.GlobRef.t list = Declare.Proof.save ~proof:lemma ~opaque ~idopt
+    in ()
 
 let vernac_exact_proof ~lemma c =
   (* spiwack: for simplicity I do not enforce that "Proof proof_term" is
      called only at the beginning of a proof. *)
   let lemma, status = Declare.Proof.by (Tactics.exact_proof c) lemma in
-  let () = Declare.Proof.save ~proof:lemma ~opaque:Opaque ~idopt:None in
+  let _ : _ list = Declare.Proof.save ~proof:lemma ~opaque:Opaque ~idopt:None in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_assumption ~atts discharge kind l nl =
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index 70f4fc7b10..1b977b8e10 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -220,7 +220,9 @@ let interp_qed_delayed ~proof ~pinfo ~st pe : Vernacstate.LemmaStack.t option =
     | Admitted ->
       Declare.Proof.save_lemma_admitted_delayed ~proof ~pinfo
     | Proved (_,idopt) ->
-      Declare.Proof.save_lemma_proved_delayed ~proof ~pinfo ~idopt in
+      let _ : _ list = Declare.Proof.save_lemma_proved_delayed ~proof ~pinfo ~idopt in
+      ()
+  in
   stack
 
 let interp_qed_delayed_control ~proof ~pinfo ~st ~control { CAst.loc; v=pe } =