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 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind/functional_principles_proofs.ml')

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