]> matita.cs.unibo.it Git - helm.git/blobdiff - components/grafite_parser/grafiteDisambiguate.ml
GrafiteAst.Print (unused) removed.
[helm.git] / components / grafite_parser / grafiteDisambiguate.ml
index 396d169e79d0c6698e35f1d1e8665365de80cddb..4ced7a0afdd04e484836fc142195c70d2d597baa 100644 (file)
@@ -326,5 +326,4 @@ let disambiguate_macro
    | GrafiteAst.Hint _
    | GrafiteAst.WLocate _ as macro ->
       metasenv,macro
-   | GrafiteAst.Quit _
-   | GrafiteAst.Print _ -> assert false
+   | GrafiteAst.Quit _ -> assert false