diff options
| author | Matej Košík | 2017-08-04 18:28:31 +0200 |
|---|---|---|
| committer | Matej Košík | 2017-11-01 08:05:37 +0100 |
| commit | f874a292c94b290a31af8e0f707ffd20ab31001b (patch) | |
| tree | eb8c4b67597cbf6adaee337717e9a09eaf9325eb /dev | |
| 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 'dev')
| -rw-r--r-- | dev/top_printers.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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) |