diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-07 23:14:26 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-06-07 23:16:37 +0200 |
| commit | 296e30761a183e64ab9c5e8dc8f2b0e48334735f (patch) | |
| tree | 57e89d73a92e9b45d3dde6625044a580b213902f /toplevel | |
| parent | 03d5d707a6d6b2cf88b7a3c9d044ec035e2efb5a (diff) | |
Removing the convenience functions from the Search API.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/search.ml | 22 | ||||
| -rw-r--r-- | toplevel/search.mli | 4 |
2 files changed, 0 insertions, 26 deletions
diff --git a/toplevel/search.ml b/toplevel/search.ml index 74a65be67..e670b59b7 100644 --- a/toplevel/search.ml +++ b/toplevel/search.ml @@ -263,28 +263,6 @@ type search_constraint = | In_Module of Names.DirPath.t | Include_Blacklist -let pattern_of_string ?env s = - let env = - match env with - | None -> Global.env () - | Some e -> e - in - let constr = Pcoq.parse_string Pcoq.Constr.lconstr_pattern s in - let (_, pat) = Constrintern.intern_constr_pattern env constr in - pat - -let dirpath_of_string_list s = - let path = String.concat "." s in - let m = Pcoq.parse_string Pcoq.Constr.global path in - let (_, qid) = Libnames.qualid_of_reference m in - let id = - try Nametab.full_name_module qid - with Not_found -> - Errors.errorlabstrm "Search.interface_search" - (str "Module " ++ str path ++ str " not found.") - in - id - type 'a coq_object = { coq_object_prefix : string list; coq_object_qualid : string list; diff --git a/toplevel/search.mli b/toplevel/search.mli index a1814b225..9f209a17e 100644 --- a/toplevel/search.mli +++ b/toplevel/search.mli @@ -57,10 +57,6 @@ type search_constraint = (** Bypass the Search blacklist *) | Include_Blacklist -val pattern_of_string : ?env:Environ.env -> string -> Pattern.constr_pattern - -val dirpath_of_string_list : string list -> Names.DirPath.t - type 'a coq_object = { coq_object_prefix : string list; coq_object_qualid : string list; |