auto and autogui... some work

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

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 521db02f3d28d3655d55e35bfc8613aa32869583..811da9ddce9e7fe6058381969c9149b09f5a1f9e 100644 (file)
--- 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)