From 9701a8bee17d66e49a5cff28dc62963c54fadc6b Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Tue, 11 Jan 2005 16:05:23 +0000 Subject: [PATCH] added search commands --- helm/ocaml/cic_transformations/tacticAst.ml | 4 ++++ helm/ocaml/cic_transformations/tacticAstPp.ml | 10 ++++++++++ 2 files changed, 14 insertions(+) diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml index 28b256c86..8c678de93 100644 --- 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 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 | [] -> "" -- 2.39.2