]> matita.cs.unibo.it Git - helm.git/commitdiff
bug fix in inline syntax
authorFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 25 Aug 2008 18:19:49 +0000 (18:19 +0000)
committerFerruccio Guidi <ferruccio.guidi@unibo.it>
Mon, 25 Aug 2008 18:19:49 +0000 (18:19 +0000)
helm/software/components/grafite_parser/grafiteParser.ml

index 38a8667d304ae511da33b6abf47971f178922726..b9f6d388fa2faa50c318383f373b322b0bde459b 100644 (file)
@@ -509,7 +509,7 @@ EXTEND
     | [ IDENT "inline"]; 
         style = OPT [ IDENT "procedural"; depth = OPT int -> depth ];
         suri = QSTRING; prefix = OPT QSTRING;
-       flavour = OPT [ IDENT "as"; attr = inline_flavour -> attr ]->
+       flavour = OPT [ "as"; attr = inline_flavour -> attr ] ->
          let style = match style with 
             | None       -> GrafiteAst.Declarative
             | Some depth -> GrafiteAst.Procedural depth