X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=8b911a60183c1ff0a7022160056e5696e8ee9dee;hb=b6ceb877c05d27705ef163488aee38e60a86886c;hp=5d138bbe06624ed27896cfb0511767ee045448a6;hpb=baa054dbb476c30576bf11b81246008a7de53462;p=helm.git diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml index 5d138bbe0..8b911a601 100644 --- a/matita/components/grafite/grafiteAst.ml +++ b/matita/components/grafite/grafiteAst.ml @@ -75,6 +75,8 @@ type ntactic = | NAssumption of loc | NRepeat of loc * ntactic | NBlock of loc * ntactic list + (* Declarative langauge *) + | Assume of loc * string * nterm (* loc, identifier, term *) type nmacro = | NCheck of loc * nterm