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

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index d436977e3..1910e34ac 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -65,6 +65,7 @@ type ntactic =
    | NGeneralize of loc * npattern
    | NId of loc
    | NIntro of loc * string
+   | NInversion of loc * CicNotationPt.term * npattern  
    | NLApply of loc * CicNotationPt.term
    | NLetIn of loc * npattern * CicNotationPt.term * string
    | NReduce of loc * [ `Normalize of bool | `Whd of bool ] * npattern