Merge PR #14004: Fix the redeclaration check for Ltac2 entry points.

Reviewed-by: gares

1 files changed, 19 insertions, 0 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 ].