From a5a65ddcf0e476384c827cdf2445bc554eae825a Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 24 Jun 2020 14:22:57 +0200
Subject: [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.
---
 plugins/funind/functional_principles_proofs.ml |  2 +-
 plugins/funind/gen_principle.ml                |  4 ++--
 plugins/funind/recdef.ml                       | 10 ++++++++--
 3 files changed, 11 insertions(+), 5 deletions(-)

(limited to 'plugins')

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
-- 
cgit v1.2.3