diff options
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 |