X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAstPp.ml;h=d064ef619fc6918452ebbc5ce935caeb36a1c027;hb=80110e17ef1d38d71473e9471ce15beddde663bb;hp=13a4690dd6408014b436687832232f13622615a2;hpb=3199f2a8428b5d19a3a803c1b03d9f90e4120f74;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 13a4690dd..d064ef619 100644
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -203,7 +203,7 @@ let pp_macro ~term_pp =
   (* real macros *)
   | Check (_, term) -> sprintf "check %s" (term_pp term)
   | Hint _ -> "hint"
-  | Inline (_,suri) -> sprintf "inline %s" suri
+  | Inline (_,suri) -> sprintf "inline \"%s\"" suri
 
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"
@@ -222,7 +222,7 @@ let pp_default what uris =
     (String.concat " " (List.map UriManager.string_of_uri uris))
 
 let pp_coercion uri do_composites arity =
-   sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity
+   sprintf "coercion \"%s\" %d (* %s *)" (UriManager.string_of_uri uri) arity
      (if do_composites then "compounds" else "no compounds")
     
 let pp_command ~term_pp ~obj_pp = function