Fix the redeclaration check for Ltac2 entry points.

Fixes #14003: Ltac2 redefinition check is broken.

4 files changed, 30 insertions, 15 deletions

diff --git a/test-suite/bugs/closed/bug_14003.v b/test-suite/bugs/closed/bug_14003.v
new file mode 100644
index 0000000000..9e7055045d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_14003.v
@@ -0,0 +1,19 @@
+Require Import Ltac2.Ltac2.
+
+Module Foo.
+
+Ltac2 foo := ().
+Ltac2 Type bar := [ BAR ].
+Ltac2 Type quz := [ .. ].
+Ltac2 Type quz ::= [ QUZ ].
+
+End Foo.
+
+Import Foo.
+
+(* Check that redeclaration checks are based on absolute names *)
+
+Ltac2 foo := ().
+Ltac2 Type bar := [ ].
+Ltac2 Type qux := [ BAR ].
+Ltac2 Type quz ::= [ QUZ ].
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index d2e74609a2..6be5ba80d5 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -381,9 +381,9 @@ let register_typedef ?(local = false) isrec types =
   in
   let () =
     let check_existing_type ({v=id},_) =
-      let qid = Libnames.make_qualid (Lib.current_dirpath false) id in
-      try let _ = Tac2env.locate_type qid in
-        user_err (str "Multiple definition of the type name " ++ pr_qualid qid)
+      let (_, kn) = Lib.make_foname id in
+      try let _ = Tac2env.interp_type kn in
+        user_err (str "Multiple definition of the type name " ++ Id.print id)
       with Not_found -> ()
     in
     List.iter check_existing_type types
@@ -417,9 +417,10 @@ let register_typedef ?(local = false) isrec types =
       in
       let () =
         let check_existing_ctor (id, _) =
-          let qid = Libnames.make_qualid (Lib.current_dirpath false) id in
-          if Tac2env.mem_constructor qid
-          then user_err (str "Constructor already defined in this module " ++ pr_qualid qid)
+          let (_, kn) = Lib.make_foname id in
+          try let _ = Tac2env.interp_constructor kn in
+            user_err (str "Constructor already defined in this module " ++ Id.print id)
+          with Not_found -> ()
         in
         List.iter check_existing_ctor cs
       in
@@ -512,9 +513,10 @@ let register_open ?(local = false) qid (params, def) =
           user_err (str "Multiple definitions of the constructor " ++ Id.print id)
       in
       let check_existing_ctor (id, _) =
-        let qid = Libnames.make_qualid (Lib.current_dirpath false) id in
-        if Tac2env.mem_constructor qid
-        then user_err (str "Constructor already defined in this module " ++ pr_qualid qid)
+          let (_, kn) = Lib.make_foname id in
+          try let _ = Tac2env.interp_constructor kn in
+            user_err (str "Constructor already defined in this module " ++ Id.print id)
+          with Not_found -> ()
       in
       let () = List.iter check_existing_ctor def in
       ()
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index 5eb57c8f9b..969b6c8e28 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -203,11 +203,6 @@ let shortest_qualid_of_constructor kn =
   let sp = KNmap.find kn tab.tab_cstr_rev in
   KnTab.shortest_qualid Id.Set.empty sp tab.tab_cstr
 
-let mem_constructor qid =
-  let tab = !nametab in
-  try ignore (KnTab.locate qid tab.tab_cstr) ; true
-  with Not_found -> false
-
 let push_type vis sp kn =
   let tab = !nametab in
   let tab_type = KnTab.push vis sp kn tab.tab_type in
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index 3800ad0198..02b34b594e 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -89,7 +89,6 @@ val locate_extended_all_ltac : qualid -> tacref list
 val shortest_qualid_of_ltac : tacref -> qualid
 
 val push_constructor : visibility -> full_path -> ltac_constructor -> unit
-val mem_constructor : qualid -> bool
 val locate_constructor : qualid -> ltac_constructor
 val locate_extended_all_constructor : qualid -> ltac_constructor list
 val shortest_qualid_of_constructor : ltac_constructor -> qualid