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

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 27f3830b6..c4ec503c7 100644
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -88,12 +88,24 @@ type ntactic =
    | Bydone of loc * just
    | ExistsElim of loc * just * string * nterm * nterm * string
    | AndElim of loc * just * nterm * string * nterm * string
+                (*
    | RewritingStep of
       loc * (string option * nterm) option * nterm *
        [ `Term of nterm | `Auto of auto_params
        | `Proof | `SolveWith of nterm ] *
        bool (* last step*)
+                   *)
+   | RewritingStep of
+      loc * nterm * [ `Term of nterm | `Auto of auto_params | `Proof | `SolveWith of nterm ] * bool (* last step*)
+   | Obtain of
+      loc * string * nterm
+   | Conclude of
+      loc * nterm
    | Thesisbecomes of loc * nterm * nterm option
+   | We_proceed_by_induction_on of loc * nterm * nterm
+   | We_proceed_by_cases_on of loc * nterm * nterm
+   | Byinduction of loc * nterm * string
+   | Case of loc * string * (string * nterm) list 
     (* This is a debug tactic to print the stack to stdout, can be safely removed *)
    | PrintStack of loc