From 5711fc6dcd9a0a566e0bbb543e9d7edb413aacf4 Mon Sep 17 00:00:00 2001
From: Kenji Maillard
Date: Mon, 4 Nov 2019 23:44:28 +0100
Subject: Prevent double definition of Ltac2 constructors inside a module; Fix
 #11046

---
 test-suite/bugs/closed/bug_11046.v | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_11046.v

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_11046.v b/test-suite/bugs/closed/bug_11046.v
new file mode 100644
index 0000000000..c73fa78473
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11046.v
@@ -0,0 +1,19 @@
+From Ltac2 Require Import Ltac2.
+
+Ltac2 Type t := [..].
+Ltac2 Type t ::= [A(int)].
+
+(* t cannot be extended with two constructors with the same name *)
+Fail Ltac2 Type t ::= [A(bool)].
+Fail Ltac2 Type t ::= [B | B(bool)].
+
+(* constructors cannot be shadowed in the same module *)
+Fail Ltac2 Type s := [A].
+
+(* constructors with the same name can be defined in distinct modules *)
+Module Other.
+  Ltac2 Type t ::= [A(bool)].
+End Other.
+Module YetAnother.
+  Ltac2 Type t' := [A].
+End YetAnother.
-- 
cgit v1.2.3