diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-08-04 18:28:31 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-11-01 08:05:37 +0100 |
| commit | f874a292c94b290a31af8e0f707ffd20ab31001b (patch) | |
| tree | eb8c4b67597cbf6adaee337717e9a09eaf9325eb /API | |
| parent | e5659c8ffe735c530a707a61c692a3af21a79a9a (diff) | |
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 "->" .
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/API/API.mli b/API/API.mli index e20793077..e82297202 100644 --- a/API/API.mli +++ b/API/API.mli @@ -5814,7 +5814,7 @@ module Vernacinterp : sig 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 |