From 45684eb8f1202665dc33bd98f1dbd46ae572757e Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 9 Apr 2019 14:25:48 +0200
Subject: [api] [proof] Alert users that `Vernacstate.Proof_global` is not to
 be used.

We alert users that `Vernacstate.Proof_global` is a Coq internal
module and should not be used to workaround lack of state threading.
---
 dev/top_printers.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 74be300134..816316487c 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -65,6 +65,7 @@ let get_current_context () =
   with Vernacstate.Proof_global.NoCurrentProof ->
     let env = Global.env() in
     Evd.from_env env, env
+  [@@ocaml.warning "-3"]
 
 (* term printers *)
 let envpp pp = let sigma,env = get_current_context () in pp env sigma
-- 
cgit v1.2.3