diff options
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 |