From 6e0855b5dc0fbebafa1e73f42993c94b2a47ae1c Mon Sep 17 00:00:00 2001
From: Matej Košík <matej.kosik@inria.fr>
Date: Thu, 8 Jun 2017 23:25:31 +0200
Subject: don't leak unqualified identifiers from the macro

---
 grammar/argextend.mlp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'grammar')

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<
-- 
cgit v1.2.3