diff options
| author | Pierre-Marie Pédrot | 2015-05-11 18:18:07 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-05-11 19:38:24 +0200 |
| commit | 2a2d418971a019202cdb78fabc7658a543f0886d (patch) | |
| tree | 0292c97712ab9ac39b1595a498aec131cbc1227f /tactics | |
| parent | 7bc1610376fac29397be39d4a06b178e8e35e66e (diff) | |
Adding a test to check whether two tactic notations conflict.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacenv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacenv.mli | 3 |
2 files changed, 5 insertions, 0 deletions
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml index ffff44d5bc..08e8bc0112 100644 --- a/tactics/tacenv.ml +++ b/tactics/tacenv.ml @@ -26,6 +26,8 @@ let interp_alias key = try KNmap.find key !alias_map with Not_found -> Errors.anomaly (str "Unknown tactic alias: " ++ KerName.print key) +let check_alias key = KNmap.mem key !alias_map + (** ML tactic extensions (TacML) *) type ml_tactic = diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli index 29677fd4ca..9410ccb389 100644 --- a/tactics/tacenv.mli +++ b/tactics/tacenv.mli @@ -23,6 +23,9 @@ val register_alias : alias -> glob_tactic_expr -> unit val interp_alias : alias -> glob_tactic_expr (** Recover the the body of an alias. Raises an anomaly if it does not exist. *) +val check_alias : alias -> bool +(** Returns [true] if an alias is defined, false otherwise. *) + (** {5 Coq tactic definitions} *) val register_ltac : bool -> bool -> Id.t -> glob_tactic_expr -> unit |