]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite_parser/grafiteParser.ml
implemented tinycals:
[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml
index 1b06b81c97fd64b26b4429956c25e9c573c7bdd5..d4c89e0e33f6b93b06f14f73981c0bc238012748 100644 (file)
@@ -266,7 +266,8 @@ EXTEND
     [
       [ SYMBOL "[" -> GrafiteAst.Branch loc
       | SYMBOL "|" -> GrafiteAst.Shift loc
-      | i = int; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
+      | i = LIST1 int SEP SYMBOL ","; SYMBOL ":" -> GrafiteAst.Pos (loc, i)
+      | SYMBOL "*"; SYMBOL ":" -> GrafiteAst.Wildcard loc
       | SYMBOL "]" -> GrafiteAst.Merge loc
       | SYMBOL ";" -> GrafiteAst.Semicolon loc
       | SYMBOL "." -> GrafiteAst.Dot loc