X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;fp=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=29dfe324b4426e25ade914f6aa5aac0be7f65677;hb=185541ccf10a6c4bf69b3db36fdc4ebc09e4cc42;hp=8b911a60183c1ff0a7022160056e5696e8ee9dee;hpb=b6ceb877c05d27705ef163488aee38e60a86886c;p=helm.git

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index 8b911a601..29dfe324b 100644
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -76,7 +76,9 @@ type ntactic =
    | 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