From f874a292c94b290a31af8e0f707ffd20ab31001b Mon Sep 17 00:00:00 2001 From: Matej Košík Date: Fri, 4 Aug 2017 18:28:31 +0200 Subject: provide "loc : Loc.t" binding within "VERNAC COMMAND EXTEND" rules Originally, it was not possible to define a new vernacular command in the following way: VERNAC COMMAND EXTEND Cmd6 CLASSIFIED AS QUERY [ "SomeCmd" ] -> [ Feedback.msg_notice ?loc (Pp.str "some message") ] END because "loc : Loc.t" was not bound. This commit fixes that, i.e. the location of the custom Vernacular command (within *.v file) is made available as "loc" variable bound on the right side of "->" . --- vernac/vernacinterp.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/vernacinterp.mli') diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli index f58d07086..84370fdc2 100644 --- a/vernac/vernacinterp.mli +++ b/vernac/vernacinterp.mli @@ -9,7 +9,7 @@ (** Interpretation of extended vernac phrases. *) type deprecation = bool -type vernac_command = Genarg.raw_generic_argument list -> unit -> unit +type vernac_command = Genarg.raw_generic_argument list -> Loc.t option -> unit val vinterp_add : deprecation -> Vernacexpr.extend_name -> vernac_command -> unit @@ -17,4 +17,4 @@ val overwriting_vinterp_add : Vernacexpr.extend_name -> vernac_command -> unit val vinterp_init : unit -> unit -val call : ?locality:bool -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit +val call : ?locality:bool -> ?loc:Loc.t -> Vernacexpr.extend_name * Genarg.raw_generic_argument list -> unit -- cgit v1.2.3