X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=components%2Fgrafite%2FgrafiteAstPp.ml;h=55736e862e2cba8aa5ee548a823691af3f7810aa;hb=6188c48d0ccbe5d8b7dbae9b8ff6de5bf984efa4;hp=941f75d9d6dae352574be19861ddc79d1775f2c5;hpb=aa576f13a6fd64586b389880dec3e47f703cd300;p=helm.git

diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml
index 941f75d9d..55736e862 100644
--- a/components/grafite/grafiteAstPp.ml
+++ b/components/grafite/grafiteAstPp.ml
@@ -154,8 +154,8 @@ let rec pp_tactic ~term_pp ~lazy_term_pp =
   | Split _ -> "split"
   | Symmetry _ -> "symmetry"
   | Transitivity (_, term) -> "transitivity " ^ term_pp term
-
-let pp_search_kind = function
+  
+  let pp_search_kind = function
   | `Locate -> "locate"
   | `Hint -> "hint"
   | `Match -> "match"
@@ -182,11 +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