diff options
| author | Emilio Jesus Gallego Arias | 2019-04-09 14:25:48 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-09 20:23:44 +0200 |
| commit | 45684eb8f1202665dc33bd98f1dbd46ae572757e (patch) | |
| tree | ed564a764c4d14262bb5345d5e9a6bbf2d79c9dc /vernac | |
| parent | e3e3e6949f1c80abec9942ee0d258b58e5a7d382 (diff) | |
[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.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/vernacentries.ml | 2 | ||||
| -rw-r--r-- | vernac/vernacstate.mli | 1 |
2 files changed, 2 insertions, 1 deletions
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"] |