]> matita.cs.unibo.it Git - helm.git/blobdiff - components/grafite_parser/grafiteDisambiguate.ml
removed abstractios for dummy metavariables when generating letins body
[helm.git] / components / grafite_parser / grafiteDisambiguate.ml
index b02d57e672ea602f704b21405f652c0eea8e5a58..76e5e6d86f13ae5257cd30e3a1e3081fecdf0eb9 100644 (file)
@@ -326,7 +326,3 @@ let disambiguate_macro
    | GrafiteAst.Hint _
    | GrafiteAst.WLocate _ as macro ->
       metasenv,macro
-   | GrafiteAst.Quit _
-   | GrafiteAst.Print _
-   | GrafiteAst.Search_pat _
-   | GrafiteAst.Search_term _ -> assert false