added search commands

diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 28b256c86000744d1ffd9b863f4d712761808d4e..8c678de93ba9d9fe6d0d91e2ac1d362efe03437d 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -88,10 +88,14 @@ type thm_flavour =
   * true means inductive, false coinductive *)
 type 'term inductive_type = string * bool * 'term * (string * 'term) list
 
+type search_kind = [ `Locate | `Hint | `Match | `Elim ]
+
 type 'term command =
   | Abort
   | Baseuri of string option (** get/set base uri *)
   | Check of 'term
+  | Search_pat of search_kind * string  (* searches with string pattern *)
+  | Search_term of search_kind * 'term  (* searches with term pattern *)
   | Proof
   | Qed of string option
       (** name.

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index bc021c134a21d23a8203f7a9876ed5a31d335201..05927a1930a9999cfac9c6f3b5c7058c5946f784 100644 (file)
--- 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
         | [] -> ""