New syntax -H1 .. Hn for clear

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

diff --git a/matita/components/grafite/grafiteAst.ml b/matita/components/grafite/grafiteAst.ml
index e251ae557dcc25ca119c4f870966fd27b32d428e..32a29c2158a98e8f1dda73f10191a6a6f6fe3d54 100644 (file)
--- a/matita/components/grafite/grafiteAst.ml
+++ b/matita/components/grafite/grafiteAst.ml
@@ -41,6 +41,7 @@ type ntactic =
    | NCases of loc * NotationPt.term * npattern  
    | NCase1 of loc * string
    | NChange of loc * npattern * NotationPt.term
+   | NClear of loc * string list
    | NConstructor of loc * int option * NotationPt.term list
    | NCut of loc * NotationPt.term
 (* | NDiscriminate of loc * NotationPt.term