Add drafts for some tactics

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

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 29dfe324b4426e25ade914f6aa5aac0be7f65677..ed757f601613cf6a0dd711860599d6454aacb8f5 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -36,6 +36,11 @@ type npattern =
 
 type auto_params = nterm list option * (string*string) list
 
+(* The additional a is for abstract *)
+type 'term aauto_params = 'term list option * (string*string) list
+
+type 'term just = [`Term of 'term | `Auto of 'term aauto_params]
+
 type ntactic =
    | NApply of loc * nterm
    | NSmartApply of loc * nterm
@@ -77,8 +82,17 @@ type ntactic =
    | NBlock of loc * ntactic list
    (* Declarative langauge *)
    (* Not the best idea to use a string directly, an abstract type for identifiers would be better *)
-   | Assume of loc * string * nterm (* loc, identifier, term *)
-   | Suppose of loc * nterm *string * nterm option
+   | Assume of loc * string * nterm * nterm option (* loc, identifier, type, eqty *)
+   | Suppose of loc * nterm *string * nterm option (* loc, assumption, identifier, eqass *)
+   | By_just_we_proved of loc * nterm just * nterm * string option * nterm option (* loc,
+   justification, conclusion, identifier, eqconcl *)
+   | We_need_to_prove of loc * nterm * string option * nterm option (* loc, newconclusion,
+   identifier, equivnewcon *)
+   | Bydone of loc * nterm just
+   (*
+   | ExistsElim of loc * nterm just * string * nterm * nterm * string
+   | AndElim of loc * nterm just * nterm * string * nterm * string
+   *)
 
 type nmacro =
   | NCheck of loc * nterm