diff options
| author | Kenji Maillard | 2019-11-01 12:44:53 +0100 |
|---|---|---|
| committer | Kenji Maillard | 2019-11-01 12:44:53 +0100 |
| commit | 7fbe716d69abb9ad7d8097a28279bbf7852a7a48 (patch) | |
| tree | e9218233cf6467fd3e66ceaeb3522afc8887a59d | |
| parent | e29ffc8c2dac2f9ea96541e95f027e29c0810499 (diff) | |
enforcing Ltac2 cosntructors name are uppercase in open types
| -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 |