From dc9c1ba86b43132691ad34bf35771b13c25696fa Mon Sep 17 00:00:00 2001
From: Kenji Maillard
Date: Fri, 1 Nov 2019 12:45:18 +0100
Subject: adding test file for Uppercase Ltac2 constructors

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

(limited to 'test-suite')

diff --git a/test-suite/bugs/closed/bug_10196.v b/test-suite/bugs/closed/bug_10196.v
new file mode 100644
index 0000000000..e2d6be56e9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10196.v
@@ -0,0 +1,26 @@
+From Ltac2 Require Import Ltac2.
+
+(* true and false are valid constructors even though they are lowercase *)
+Ltac2 Eval true.
+Ltac2 Eval false.
+
+(* Otherwise constructors have to be Uppercase *)
+Ltac2 Type good_constructor := [Uppercased].
+Ltac2 Type good_constructors := [Uppercased1 | Uppercased2].
+
+Ltac2 Eval Uppercased2.
+
+Fail Ltac2 Type bad_constructor := [ notUppercased ].
+Fail Ltac2 Type bad_constructors := [ | notUppercased1 | notUppercased2 ].
+
+Fail Ltac2 Eval notUppercased2.
+
+(* And the same for open types*)
+Ltac2 Type open_type := [ .. ].
+Fail Ltac2 Type open_type ::= [ notUppercased ].
+Ltac2 Type open_type ::= [ Uppercased ].
+
+Fail Ltac2 Eval notUppercased.
+Ltac2 Eval Uppercased.
+
+Fail Ltac2 Type foo ::= [ | bar1 | bar2 ].
-- 
cgit v1.2.3