- transcript: now outputs includes and coercions correctly

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

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 5644d33d3e8a0cd144a20661d18d31b026de342f..d064ef619fc6918452ebbc5ce935caeb36a1c027 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/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"
@@ -219,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