diff options
| author |  Matej Košík <matej.kosik@inria.fr> | 2017-06-08 23:25:31 +0200 |
|---|---|---|
| committer | Matej Košík <matej.kosik@inria.fr> | 2017-06-10 13:39:13 +0200 |
| commit | 6e0855b5dc0fbebafa1e73f42993c94b2a47ae1c (patch) | |
| tree | c1090d2475ba8aaf5b8e247b7fad6638899271e7 /grammar | |
| parent | dffba98368b5b1156e1933dc7377317281c57491 (diff) | |
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< |