Fixed a bug in deep_eq: we generated new clauses but neglected the

[helm.git] / helm / software / components / grafite / grafiteAst.ml

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 7754102c6ac36052b936d875e26985c188071a4f..1910e34ac949d279cae975f146920745f2368189 100644 (file)
--- 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
@@ -64,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