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 "->" .

0 files changed, 0 insertions, 0 deletions