Procedural: some improvements

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

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 14802a629e8cd32360a33c33d1550f506fc50b84..1321f613b82e91a5acc8e793d14c76d49f687624 100644 (file)
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -117,7 +117,9 @@ EXTEND
   ];
   int: [ [ num = NUMBER -> int_of_string num ] ];
   intros_spec: [
-    [ num = OPT [ num = int -> num ]; idents = OPT ident_list0 ->
+    [ OPT [ IDENT "names" ]; 
+      num = OPT [ num = int -> num ]; 
+      idents = OPT ident_list0 ->
         let idents = match idents with None -> [] | Some idents -> idents in
         num, idents
     ]