From 0c748e670ef1a81cb35c1cc55892dba141c25930 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 2 Apr 2020 01:41:20 -0400
Subject: [proof] Merge `Proof_global` into `Declare`

We place creation and saving of interactive proofs in the same module;
this will allow to make `proof_entry` private, improving invariants
and control over clients, and to reduce the API [for example next
commit will move abstract declaration into this module, removing the
exported ad-hoc `build_constant_by_tactic`]

Next step will be to unify all the common code in the interactive /
non-interactive case; but we need to tweak the handling of obligations
first.
---
 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 ad0891b567..7b2ce671a3 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -847,7 +847,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   in
   let lemma, _ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
   let () =
-    Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent ~idopt:None
+    Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None
   in
   evd
 
-- 
cgit v1.2.3