diff options
| author | Maxime Dénès | 2019-04-29 16:38:26 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-29 16:38:26 +0200 |
| commit | f08880552350310df8a60ec37d6ada9d0ef1b40f (patch) | |
| tree | 3af1ff908cd64f00ec0c871a780449f9a5de529c /vernac | |
| parent | 2ad60e808052d163ca84094131b453f2bccc3143 (diff) | |
| parent | 45684eb8f1202665dc33bd98f1dbd46ae572757e (diff) | |
Merge PR #9935: [api] [proof] Alert users that `Vernacstate.Proof_global` is not to be used.
Ack-by: ejgallego
Ack-by: gares
Reviewed-by: maximedenes
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 3a305c3b61..e44d68b87d 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2627,7 +2627,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"] |