X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=4ced7a0afdd04e484836fc142195c70d2d597baa;hb=4c3c77a722996633ec810a7fa547f52872124074;hp=b02d57e672ea602f704b21405f652c0eea8e5a58;hpb=50fd7ca0b4e54ee341517ea653b3862b9655d4c5;p=helm.git diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index b02d57e67..4ced7a0af 100644 --- 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