X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=27f3830b679cfd43b453eb9a78980e74abe9e48b;hb=3fab56d1663ba3d5aeb9207612279e0bb0edbb8c;hp=c15414df5bd40251fad484761735999939d9c0ef;hpb=dd627e471392375ca7b6dad78a931a8682e06dbe;p=helm.git

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index c15414df5..27f3830b6 100644
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -90,10 +90,12 @@ type ntactic =
    | AndElim of loc * just * nterm * string * nterm * string
    | RewritingStep of
       loc * (string option * nterm) option * nterm *
-       [ `Term of nterm | `Auto of (string*string) list
+       [ `Term of nterm | `Auto of auto_params
        | `Proof | `SolveWith of nterm ] *
        bool (* last step*)
    | Thesisbecomes of loc * nterm * nterm option
+    (* This is a debug tactic to print the stack to stdout, can be safely removed *)
+   | PrintStack of loc 
 
 type nmacro =
   | NCheck of loc * nterm