X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=811da9ddce9e7fe6058381969c9149b09f5a1f9e;hb=ce5018fb3004d79fd16301dfc0fd9370d59ba4fc;hp=521db02f3d28d3655d55e35bfc8613aa32869583;hpb=b8254cf86275b9d78b30a0b14974a6f23ad9be24;p=helm.git

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 521db02f3..811da9ddc 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -96,7 +96,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
      "applyS " ^ term_pp term ^
       String.concat " " 
         (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
-  | Auto (_,params) -> "auto " ^ 
+  | AutoBatch (_,params) -> "auto batch " ^ 
       String.concat " " 
         (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
   | Assumption _ -> "assumption"
@@ -227,6 +227,9 @@ let pp_macro ~term_pp =
   (* real macros *)
   | Check (_, term) -> Printf.sprintf "check %s" (term_pp term)
   | Hint _ -> "hint"
+  | AutoInteractive (_,params) -> "auto " ^ 
+      String.concat " " 
+        (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
   | Inline (_, style, suri, prefix) ->  
       Printf.sprintf "inline %s\"%s\"%s" (style_pp style) suri (prefix_pp prefix)