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 +++
 toplevel/metasyntax.ml | 7 +++++++
 3 files changed, 12 insertions(+)

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
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index f4fabc4d3a..300bf5b490 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -84,8 +84,14 @@ type tactic_grammar_obj = {
   tacobj_body : Tacexpr.glob_tactic_expr
 }
 
+let check_key key =
+  if Tacenv.check_alias key then
+    error "Conflicting tactic notations keys. This can happen when including \
+    twice the same module."
+
 let cache_tactic_notation (_, tobj) =
   let key = tobj.tacobj_key in
+  let () = check_key key in
   Tacenv.register_alias key tobj.tacobj_body;
   Egramcoq.extend_tactic_grammar key tobj.tacobj_tacgram;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp
@@ -97,6 +103,7 @@ let open_tactic_notation i (_, tobj) =
 
 let load_tactic_notation i (_, tobj) =
   let key = tobj.tacobj_key in
+  let () = check_key key in
   (** Only add the printing and interpretation rules. *)
   Tacenv.register_alias key tobj.tacobj_body;
   Pptactic.declare_notation_tactic_pprule key tobj.tacobj_tacpp;
-- 
cgit v1.2.3