X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=5b10a5465cc5fc9ad68889fc87a8236ad3bede2c;hb=c8767b56c0a77fa52efb3815524620602709922b;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..5b10a5465 100644
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -43,7 +43,7 @@ type 'lazy_term reduction =
 
 type 'ident intros_spec = int option * 'ident option list
 
-type 'term auto_params = 'term list * (string*string) list
+type 'term auto_params = 'term list option * (string*string) list
 
 type 'term just =
  [ `Term of 'term
@@ -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