Merge PR #11019: enforcing Ltac2 constructor name are uppercased

Reviewed-by: ppedrot

1 files changed, 26 insertions, 0 deletions

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 ].