diff options
Diffstat (limited to 'vernac/vernacstate.mli')
| -rw-r--r-- | vernac/vernacstate.mli | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli index b4d478d12d..ed20cb935a 100644 --- a/vernac/vernacstate.mli +++ b/vernac/vernacstate.mli @@ -14,8 +14,10 @@ type t = { shallow : bool (* is the state trimmed down (libstack) *) } -val freeze_interp_state : Summary.marshallable -> t +val freeze_interp_state : marshallable:bool -> t val unfreeze_interp_state : t -> unit +val make_shallow : t -> t + (* WARNING: Do not use, it will go away in future releases *) val invalidate_cache : unit -> unit |