Partially restore the suppose tactic

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

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 5d138bbe06624ed27896cfb0511767ee045448a6..29dfe324b4426e25ade914f6aa5aac0be7f65677 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -75,6 +75,10 @@ type ntactic =
    | NAssumption of loc
    | NRepeat of loc * 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
 
 type nmacro =
   | NCheck of loc * nterm