From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 8 Jan 2010 08:12:06 +0000 (+0000)
Subject: applyS
X-Git-Tag: make_still_working~3141
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d5524a1863254efc83b44042bcce78678a95d737;p=helm.git

applyS
---

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