new tactic constructor: @[n]

[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 c84bf99fa1f250a336c79d80e6c3a85dad0af451..1d3b21392045d561ef21f7c59050790f6194e5ec 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -55,6 +55,7 @@ type ntactic =
    | NCases of loc * CicNotationPt.term * npattern  
    | NCase1 of loc * string
    | NChange of loc * npattern * CicNotationPt.term
+   | NConstructor of loc * int option
    | NElim of loc * CicNotationPt.term * npattern  
    | NGeneralize of loc * npattern
    | NId of loc