X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=366c0e264fe0d201fe071d6cf4b6fad8bf7f8fa0;hb=666e2a3fcbfffd2df99650e3404965e95e6b352b;hp=5644d33d3e8a0cd144a20661d18d31b026de342f;hpb=e11e617809bbf3757ddfcbd6ef6d28d20e14a4f0;p=helm.git

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 5644d33d3..366c0e264 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -75,7 +75,10 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   function
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
-  | ApplyS (_, term) -> "applyS " ^ term_pp term
+  | ApplyS (_, term, params) ->
+     "applyS " ^ term_pp term ^
+      String.concat " " 
+        (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
   | Auto (_,params) -> "auto " ^ 
       String.concat " " 
         (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
@@ -200,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"
@@ -223,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"