3 files changed, 13 insertions, 2 deletions
diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 6b7b75f0d4..9c8e29c46f 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
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