diff options
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 |