GrafiteAst.Print (unused) removed.

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index b02d57e672ea602f704b21405f652c0eea8e5a58..4ced7a0afdd04e484836fc142195c70d2d597baa 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -326,7 +326,4 @@ let disambiguate_macro
    | GrafiteAst.Hint _
    | GrafiteAst.WLocate _ as macro ->
       metasenv,macro
-   | GrafiteAst.Quit _
-   | GrafiteAst.Print _
-   | GrafiteAst.Search_pat _
-   | GrafiteAst.Search_term _ -> assert false
+   | GrafiteAst.Quit _ -> assert false