diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-16 16:28:39 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-16 16:28:39 +0200 |
| commit | db522eb68496f56c11d43cb269c4d14943f334af (patch) | |
| tree | 871b7230294a646814768a325d94a4ed54b7aa36 /grammar | |
| parent | 1d3703be3ab41d016c776bb29d9f5eff0cdb401d (diff) | |
| parent | 6e0855b5dc0fbebafa1e73f42993c94b2a47ae1c (diff) | |
Merge PR#759: don't leak unqualified identifiers from the macro
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.mlp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 36b9d612a..8aecf0e0c 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -178,7 +178,7 @@ let declare_vernac_argument loc s pr cl = let se = mlexpr_of_string s in let wit = <:expr< $lid:"wit_"^s$ >> in let pr_rules = match pr with - | None -> <:expr< fun _ _ _ _ -> str $str:"[No printer for "^s^"]"$ >> + | None -> <:expr< fun _ _ _ _ -> Pp.str $str:"[No printer for "^s^"]"$ >> | Some pr -> <:expr< fun _ _ _ -> $lid:pr$ >> in declare_str_items loc [ <:str_item< |