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.
---
 pretyping/vernacexpr.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/vernacexpr.ml b/pretyping/vernacexpr.ml
index 304a5dadd5..71a2e8cb8f 100644
--- a/pretyping/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml
@@ -135,7 +135,8 @@ type search_restriction =
 
 type rec_flag       = bool (* true = Rec;           false = NoRec          *)
 type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
-type opacity_flag   = Opaque | Transparent
+type opacity_flag   = Proof_global.opacity_flag = Opaque | Transparent
+ [@ocaml.deprecated "Please use [Proof_global.opacity_flag]"]
 type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
-- 
cgit v1.2.3