diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 03:40:45 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 17:38:19 +0100 |
| commit | dc664b3b0c6f6f5eeba0c1092efc3f4537cdf657 (patch) | |
| tree | 228d0aeba91a663b947625fd58cebe5bf4537f08 /vernac/vernacinterp.mli | |
| parent | d7a5f439de0208c4a543a81158107b8ccecb6ced (diff) | |
[plugins] Prepare plugin API for functional handling of state.
To this purpose we allow plugins to register functions that will
modify the state.
This is not used yet, but will be used soon when we remove the global
handling of the proof state.
Diffstat (limited to 'vernac/vernacinterp.mli')
| -rw-r--r-- | vernac/vernacinterp.mli | 16 |
1 files changed, 10 insertions, 6 deletions
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index 84370fdc2..1c66b1c04 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -9,12 +9,16 @@ (** Interpretation of extended vernac phrases. *) type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit -val vinterp_add : deprecation -> Vernacexpr.extend_name -> - vernac_command -> unit -val overwriting_vinterp_add : - Vernacexpr.extend_name -> vernac_command -> 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 overwriting_vinterp_add : Vernacexpr.extend_name -> vernac_command -> unit val vinterp_init : unit -> unit -val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit + +val call : ?locality:bool -> ?loc:Loc.t -> + Vernacexpr.extend_name * Genarg.raw_generic_argument list -> + Vernacstate.t -> Vernacstate.t |