- | IDENT "notation"; (l1, assoc, prec, l2) = notation ->
- GrafiteAst.Notation (loc, l1, assoc, prec, l2)
- | IDENT "interpretation"; (symbol, args, l3) = interpretation ->
- GrafiteAst.Interpretation (loc, (symbol, args), l3)
+ | IDENT "notation"; (dir, l1, assoc, prec, l2) = notation ->
+ GrafiteAst.Notation (loc, dir, l1, assoc, prec, l2)
+ | IDENT "interpretation"; id = QSTRING;
+ (symbol, args, l3) = interpretation ->
+ GrafiteAst.Interpretation (loc, id, (symbol, args), l3)
+ | IDENT "metadata"; [ IDENT "dependency" | IDENT "baseuri" ] ; URI ->
+ (** metadata commands lives only in .moo, where they are in marshalled
+ * form *)
+ raise (CicNotationParser.Parse_error (loc, "metadata not allowed here"))