diff options
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 16 |
1 files changed, 14 insertions, 2 deletions
diff --git a/API/API.mli b/API/API.mli index 535f6a29b..d4f0872a3 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2060,6 +2060,8 @@ end module States : sig + type state + val with_state_protection_on_exception : ('a -> 'b) -> 'a -> 'b val with_state_protection : ('a -> 'b) -> 'a -> 'b end @@ -4512,6 +4514,9 @@ end module Proof_global : sig + + type state + type proof_mode = { name : string; set : unit -> unit ; @@ -5787,6 +5792,13 @@ end module Vernacentries : sig + + type interp_state = { (* TODO: inline records in OCaml 4.03 *) + system : States.state; (* summary + libstack *) + proof : Proof_global.state; (* proof state *) + shallow : bool (* is the state trimmed down (libstack) *) + } + val dump_global : Libnames.reference Misctypes.or_by_notation -> unit val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr -> Evd.evar_map * Redexpr.red_expr) Hook.t @@ -5814,11 +5826,11 @@ end module Stm : sig type doc - type state val get_doc : Feedback.doc_id -> doc + val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] end (************************************************************************) |