X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=24d37c4f318d8c1f0ee1b90b6521d5d6333861fa;hb=679f6296c9a979213425104fa606809d9f1e3bad;hp=20d57ef9e5ab6cc63b92778d972fdf4f8a952bc5;hpb=36eecd95ced29b1925913c8cfaf804c472599e66;p=helm.git

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 20d57ef9e..24d37c4f3 100644
--- 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)