Changes to declarative tactics, implementation of equality chain

[helm.git] / matita / components / grafite / grafiteAst.ml

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index c15414df5bd40251fad484761735999939d9c0ef..27f3830b679cfd43b453eb9a78980e74abe9e48b 100644 (file)
--- 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