From 7fbe716d69abb9ad7d8097a28279bbf7852a7a48 Mon Sep 17 00:00:00 2001
From: Kenji Maillard
Date: Fri, 1 Nov 2019 12:44:53 +0100
Subject: enforcing Ltac2 cosntructors name are uppercase in open types

---
 user-contrib/Ltac2/tac2entries.ml | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/user-contrib/Ltac2/tac2entries.ml b/user-contrib/Ltac2/tac2entries.ml
index 9c8e29c46f..92bc49346f 100644
--- a/user-contrib/Ltac2/tac2entries.ml
+++ b/user-contrib/Ltac2/tac2entries.ml
@@ -489,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
-- 
cgit v1.2.3