]> matita.cs.unibo.it Git - helm.git/commitdiff
applyS
authorAndrea Asperti <andrea.asperti@unibo.it>
Fri, 8 Jan 2010 08:12:06 +0000 (08:12 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Fri, 8 Jan 2010 08:12:06 +0000 (08:12 +0000)
helm/software/components/grafite/grafiteAst.ml

index 7754102c6ac36052b936d875e26985c188071a4f..d436977e381270bf415117c99b9dac3e2534406a 100644 (file)
@@ -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