Merge PR #11019: enforcing Ltac2 constructor name are uppercased

Reviewed-by: ppedrot

4 files changed, 41 insertions, 2 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 ].
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 6b7b75f0d4..92bc49346f 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -394,6 +394,13 @@ let register_typedef ?(local = false) isrec types =
       | (id, _) :: _ ->
         user_err (str "Multiple definitions of the constructor " ++ Id.print id)
       in
+      let () =
+        let check_uppercase_ident (id,_) =
+          if not (Tac2env.is_constructor_id id)
+          then user_err (str "Constructor name should start with an uppercase letter " ++ Id.print id)
+        in
+        List.iter check_uppercase_ident cs
+      in
       ()
     | CTydRec ps ->
       let same_name (id1, _, _) (id2, _, _) = Id.equal id1 id2 in
@@ -482,6 +489,8 @@ let register_open ?(local = false) qid (params, def) =
       | _ -> assert false
     in
     let map (id, tpe) =
+      if not (Tac2env.is_constructor_id id)
+      then user_err (str "Constructor name should start with an uppercase letter " ++ Id.print id) ;
       let tpe = List.map intern_type tpe in
       { edata_name = id; edata_args = tpe }
     in
diff --git a/user-contrib/Ltac2/tac2env.ml b/user-contrib/Ltac2/tac2env.ml
index 959a912ad2..5f9dc3798a 100644
--- a/user-contrib/Ltac2/tac2env.ml
+++ b/user-contrib/Ltac2/tac2env.ml
@@ -289,8 +289,7 @@ let wit_ltac2_quotation = Genarg.make0 "ltac2:quotation"
 let () = Geninterp.register_val0 wit_ltac2 None
 let () = Geninterp.register_val0 wit_ltac2_quotation None
 
-let is_constructor qid =
-  let (_, id) = repr_qualid qid in
+let is_constructor_id id =
   let id = Id.to_string id in
   assert (String.length id > 0);
   match id with
@@ -299,3 +298,7 @@ let is_constructor qid =
     match id.[0] with
     | 'A'..'Z' -> true
     | _ -> false
+
+let is_constructor qid =
+  let (_, id) = repr_qualid qid in
+  is_constructor_id id
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli
index 1dfc3400a1..670c8735ee 100644
--- a/user-contrib/Ltac2/tac2env.mli
+++ b/user-contrib/Ltac2/tac2env.mli
@@ -151,4 +151,5 @@ val wit_ltac2_quotation : (Id.t Loc.located, Id.t, Util.Empty.t) genarg_type
 
 (** {5 Helper functions} *)
 
+val is_constructor_id : Id.t -> bool
 val is_constructor : qualid -> bool