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.
---
 vernac/vernacentries.ml | 2 +-
 vernac/vernacstate.mli  | 1 +
 2 files changed, 2 insertions(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 02db75c0f9..7af4b245a2 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2632,7 +2632,7 @@ let interp ?(verbosely=true) ?proof ~st cmd =
   try vernac_timeout (fun st ->
       let v_mod = if verbosely then Flags.verbosely else Flags.silently in
       let pstate = v_mod (interp_control ?proof ~st) cmd in
-      Vernacstate.Proof_global.set pstate;
+      Vernacstate.Proof_global.set pstate [@ocaml.warning "-3"];
       Vernacstate.freeze_interp_state ~marshallable:false
     ) st
   with exn ->
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index b79f97796f..dff81ad9bb 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -82,3 +82,4 @@ module Proof_global : sig
   val copy_terminators : src:t option -> tgt:t option -> t option
 
 end
+[@@ocaml.deprecated "This module is internal and should not be used, instead, thread the proof state"]
-- 
cgit v1.2.3