X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=366c0e264fe0d201fe071d6cf4b6fad8bf7f8fa0;hb=9747f688a8624d819e07e7139df68a919f76b07d;hp=13a4690dd6408014b436687832232f13622615a2;hpb=76917216be769918258c90e486bb7c06d81b70b4;p=helm.git

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 13a4690dd..366c0e264 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/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"
@@ -226,6 +226,7 @@ let pp_coercion uri do_composites arity =
      (if do_composites then "compounds" else "no compounds")
     
 let pp_command ~term_pp ~obj_pp = function
+  | Index (_,_,uri) -> "Indexing " ^ UriManager.string_of_uri uri
   | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i
   | Default (_,what,uris) -> pp_default what uris
   | Drop _ -> "drop"