From 3f6c0abc4d434d14d47681e4142ff7b927294f64 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 21 May 2014 18:07:48 +0200
Subject: Allowing Ltac definitions that may be unusable because of a built-in
 parsing rule.

---
 tactics/tacenv.ml | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 6dc11510d4..df01b486c2 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -191,15 +191,15 @@ let make_absolute_name ident repl =
       else let id = Constrexpr_ops.coerce_reference_to_id ident in
              Some id, Lib.make_kn id
     in
-      if KNmap.mem kn !mactab then
-        if repl then id, kn
-        else
-          Errors.user_err_loc (loc, "",
-                       str "There is already an Ltac named " ++ pr_reference ident ++ str".")
-      else if is_atomic_kn kn then
-        Errors.user_err_loc (loc, "",
-                     str "Reserved Ltac name " ++ pr_reference ident ++ str".")
-      else id, kn
+    let () = if KNmap.mem kn !mactab && not repl then
+      Errors.user_err_loc (loc, "",
+        str "There is already an Ltac named " ++ pr_reference ident ++ str".")
+    in
+    let () = if is_atomic_kn kn then
+      msg_warning (str "The Ltac name " ++ pr_reference ident ++
+        str " may be unusable because of a conflict with a notation.")
+    in
+    id, kn
   with Not_found ->
     Errors.user_err_loc (loc, "",
                  str "There is no Ltac named " ++ pr_reference ident ++ str ".")
-- 
cgit v1.2.3