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/invfun.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

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

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 1809526356..b9d5ebf57c 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -818,7 +818,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	 ignore (Pfedit.by
 		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
 						      (proving_tac i))));
-	 (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+         (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
 	 let finfo = find_Function_infos (fst f_as_constant) in
 	 (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
 	 let _,lem_cst_constr = Evd.fresh_global
@@ -879,7 +879,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
 	      (proving_tac i)))) ;
-	 (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+         (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
 	 let finfo = find_Function_infos (fst f_as_constant) in
 	 let _,lem_cst_constr = Evd.fresh_global
 				  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
-- 
cgit v1.2.3