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 "->" .
---
 API/API.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'API')

diff --git a/API/API.mli b/API/API.mli
index e207930771..e82297202c 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
-- 
cgit v1.2.3