diff options
Diffstat (limited to 'API/API.mli')
| -rw-r--r-- | API/API.mli | 33 |
1 files changed, 20 insertions, 13 deletions
diff --git a/API/API.mli b/API/API.mli index 704f1a3569..8a4a6cc891 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5929,14 +5929,30 @@ sig Names.Id.t end +module Vernacstate : +sig + + type t = { (* 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) *) + } + + (* XXX: This should not be exported *) + val freeze_interp_state : Summary.marshallable -> t + val unfreeze_interp_state : t -> unit + +end + module Vernacinterp : sig + type deprecation = bool - type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit + type vernac_command = + Genarg.raw_generic_argument list -> Loc.t option -> Vernacstate.t -> Vernacstate.t - val vinterp_add : deprecation -> Vernacexpr.extend_name -> - vernac_command -> unit + val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit end @@ -5958,15 +5974,6 @@ 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 freeze_interp_state : Summary.marshallable -> interp_state - val unfreeze_interp_state : interp_state -> unit - 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 @@ -5998,7 +6005,7 @@ sig val get_doc : Feedback.doc_id -> doc val state_of_id : doc:doc -> - Stateid.t -> [ `Valid of Vernacentries.interp_state option | `Expired | `Error of exn ] + Stateid.t -> [ `Valid of Vernacstate.t option | `Expired | `Error of exn ] end (************************************************************************) |