]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite/grafiteParser.ml
1. metadata are no longer stored in .moo files.
[helm.git] / helm / ocaml / grafite / grafiteParser.ml
index 3d0ea500bc9034d858a2c7f213bf63e6f92231fd..64db522950c31e50e788c07878ced0dc5775d2d9 100644 (file)
@@ -492,10 +492,6 @@ EXTEND
     | 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 (HExtlib.Localized (loc,CicNotationParser.Parse_error "metadata not allowed here"))
 
     | IDENT "dump" -> GrafiteAst.Dump loc
     | IDENT "render"; u = URI ->