diff options
Diffstat (limited to 'vernac/vernacstate.ml')
| -rw-r--r-- | vernac/vernacstate.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml index 9ab2d00fc2..6eb618ad0a 100644 --- a/vernac/vernacstate.ml +++ b/vernac/vernacstate.ml @@ -34,6 +34,8 @@ type t = { shallow : bool (* is the state trimmed down (libstack) *) } +let pstate st = Option.map Proof_global.get_current_pstate st.proof + let s_cache = ref None let s_proof = ref None |