From e87288450d4d9e49ac91d179714a73bd0147c0d7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sat, 19 May 2018 16:51:55 +0200
Subject: [api] Move `opacity_flag` to `Proof_global`.

`Proof_global` is the main consumer of the flag, which doesn't seem to
belong to the AST as plugins show.

This will allow the vernac AST to be placed in `vernac` indeed.
---
 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 3801fec4b3..ccf109ce1b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1013,7 +1013,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
   lemma_type
   (Lemmas.mk_hook (fun _ _ -> ()));
   ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
-  Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))); 
+  Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)));
   evd
 
 
-- 
cgit v1.2.3