X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=d436977e381270bf415117c99b9dac3e2534406a;hb=fa6d1f3df955464343b365114be1071fc0b0cd18;hp=7754102c6ac36052b936d875e26985c188071a4f;hpb=2dd6e8f11fa3ac2995f326ecb742d9b4e8948fce;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