whelp locate now accepts * and ?

[helm.git] / components / grafite / grafiteAstPp.ml

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 6b618c6ac46ad7c2efcc00e75ffedb031147f721..de6200e0925134bdcc02938a0cdf83b3105923c8 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -168,7 +168,7 @@ let pp_macro ~term_pp =
   (* Whelp *)
   | WInstance (_, term) -> "whelp instance " ^ term_pp term
   | WHint (_, t) -> "whelp hint " ^ term_pp t
-  | WLocate (_, s) -> "whelp locate " ^ s
+  | WLocate (_, s) -> "whelp locate \"" ^ s ^ "\""
   | WElim (_, t) -> "whelp elim " ^ term_pp t
   | WMatch (_, term) -> "whelp match " ^ term_pp term
   (* real macros *)