added the geniric

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

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 20d57ef9e5ab6cc63b92778d972fdf4f8a952bc5..24d37c4f318d8c1f0ee1b90b6521d5d6333861fa 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -73,8 +73,9 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Absurd (_, term) -> "absurd" ^ term_pp term
   | Apply (_, term) -> "apply " ^ term_pp term
   | ApplyS (_, term) -> "applyS " ^ term_pp term
-  | Auto (_,_,_,Some kind,_) -> "auto " ^ kind
-  | Auto _ -> "auto"
+  | Auto (_,params) -> "auto " ^ 
+      String.concat " " 
+        (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params)
   | Assumption _ -> "assumption"
   | Change (_, where, with_what) ->
       sprintf "change %s with %s" (pp_tactic_pattern where) (lazy_term_pp with_what)