X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgrafite_parser%2FgrafiteDisambiguate.ml;fp=helm%2Focaml%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=3c79cc0405806d1cd4b01f88b1eacbcbfbe56985;hb=dbb9f64a437b4abda0b9f47a527ab6135d596e28;hp=9e52f92b17fd2d7382be7e4f07589fbb885ba4e0;hpb=024819eeb7fcd370114ceb3dffc7907db92ab640;p=helm.git

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
index 9e52f92b1..3c79cc040 100644
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
@@ -238,7 +238,6 @@ let disambiguate_command status =
   | GrafiteAst.Dump _
   | GrafiteAst.Include _
   | GrafiteAst.Interpretation _
-  | GrafiteAst.Metadata _
   | GrafiteAst.Notation _
   | GrafiteAst.Qed _
   | GrafiteAst.Render _