X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=d436977e381270bf415117c99b9dac3e2534406a;hb=d5524a1863254efc83b44042bcce78678a95d737;hp=7754102c6ac36052b936d875e26985c188071a4f;hpb=2ab389523157f09ac9f79743ee7e8d52aabca1ee;p=helm.git

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 7754102c6..d436977e3 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -51,6 +51,7 @@ type 'term just =
 
 type ntactic =
    | NApply of loc * CicNotationPt.term
+   | NSmartApply of loc * CicNotationPt.term
    | NAssert of loc * ((string * [`Decl of CicNotationPt.term | `Def of CicNotationPt.term * CicNotationPt.term]) list * CicNotationPt.term) list
    | NCases of loc * CicNotationPt.term * npattern  
    | NCase1 of loc * string