From 2a2d418971a019202cdb78fabc7658a543f0886d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 11 May 2015 18:18:07 +0200
Subject: Adding a test to check whether two tactic notations conflict.

---
 tactics/tacenv.ml  | 2 ++
 tactics/tacenv.mli | 3 +++
 2 files changed, 5 insertions(+)

(limited to 'tactics')

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
-- 
cgit v1.2.3