X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=inline;f=helm%2Focaml%2Fcic_transformations%2FtacticAstPp.ml;h=05927a1930a9999cfac9c6f3b5c7058c5946f784;hb=e097097df79962ad19cc1c4b75e8814b41fa1c64;hp=bc021c134a21d23a8203f7a9876ed5a31d335201;hpb=6d5e3e4ec26caa02e4cd3e29fa8c4a989f8b0352;p=helm.git

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index bc021c134..05927a193 100644
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -96,6 +96,12 @@ let pp_flavour = function
   | `Remark -> "Remark"
   | `Theorem -> "Theorem"
 
+let pp_search_kind = function
+  | `Locate -> "locate"
+  | `Hint -> "hint"
+  | `Match -> "match"
+  | `Elim -> "elim"
+
 let pp_command = function
   | Abort -> "Abort"
   | Baseuri (Some uri) -> sprintf "Baseuri \"%s\"" uri
@@ -107,6 +113,10 @@ let pp_command = function
   | Quit -> "Quit"
   | Redo None -> "Redo"
   | Redo (Some n) -> sprintf "Redo %d" n
+  | 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) (pp_term term)
   | Inductive (params, types) ->
       let pp_params = function
         | [] -> ""