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 "->" .
---
 dev/top_printers.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 70f7c4283f..35956477df 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -503,7 +503,7 @@ let _ =
       (function
          [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
-           (fun () -> in_current_context constr_display c)
+           (fun _ -> in_current_context constr_display c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> pp (CErrors.print e)
@@ -519,7 +519,7 @@ let _ =
       (function
          [c] when genarg_tag c = unquote (topwit wit_constr) && true ->
            let c = out_gen (rawwit wit_constr) c in
-           (fun () -> in_current_context print_pure_constr c)
+           (fun _ -> in_current_context print_pure_constr c)
        | _ -> failwith "Vernac extension: cannot occur")
   with
     e -> pp (CErrors.print e)
-- 
cgit v1.2.3