From 4a865fbce27d2b5ba0824ad52db0fea36ede0a9e Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 25 Mar 2021 15:02:51 +0100
Subject: Fix the redeclaration check for Ltac2 entry points.

Fixes #14003: Ltac2 redefinition check is broken.
---
 test-suite/bugs/closed/bug_14003.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_14003.v

(limited to 'test-suite')

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