X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteParser.ml;h=1321f613b82e91a5acc8e793d14c76d49f687624;hb=2c4dd8bdb55dff0c590ee6abd94aab0e7417c626;hp=14802a629e8cd32360a33c33d1550f506fc50b84;hpb=4609a07e2fe4343d94832fcaf0936223f83ba71c;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 14802a629..1321f613b 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/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
     ]