constructor accepts the arguments of the constructor...

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 8232aa672abda946479f7d75ab9ed44275b49005..6b80c32cf0c411ef948933e9bf7778fc7aada208 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -253,9 +253,9 @@ EXTEND
         G.NCases (loc, what, where)
     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> 
         G.NChange (loc, what, with_what)
-    | SYMBOL "@"; num = OPT NUMBER -> 
+    | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term -> 
         G.NConstructor (loc,
-           match num with None -> None | Some x -> Some (int_of_string x))
+           (match num with None -> None | Some x -> Some (int_of_string x)),l)
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
         G.NElim (loc, what, where)
     | IDENT "ngeneralize"; p=pattern_spec ->