diff options
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"] |