libraryclean fixed to eradicate files generated from .ma files that do not

[helm.git] / components / grafite / grafiteAstPp.ml

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index b95df8d366d3a3daf5d70a8efeaac7a20c4875e7..d35a8af114936570f77f4be4366d655d04bd0b2b 100644 (file)
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -182,12 +182,6 @@ let pp_macro ~term_pp =
   (* real macros *)
   | Check (_, term) -> sprintf "Check %s" (term_pp term)
   | Hint _ -> "hint"
-  | Search_pat (_, kind, pat) ->
-      sprintf "search %s \"%s\"" (pp_search_kind kind) pat
-  | Search_term (_, kind, term) ->
-      sprintf "search %s %s" (pp_search_kind kind) (term_pp term)
-  | Print (_, name) -> sprintf "Print \"%s\"" name
-  | Quit _ -> "Quit"
 
 let pp_associativity = function
   | Gramext.LeftA -> "left associative"