diff options
| author | Kenji Maillard | 2019-10-31 14:40:01 +0100 |
|---|---|---|
| committer | Kenji Maillard | 2019-10-31 17:04:19 +0100 |
| commit | e29ffc8c2dac2f9ea96541e95f027e29c0810499 (patch) | |
| tree | 15fda15b99514b94feec343f7c1722a73f024579 | |
| parent | bc70919118fe5450c3bb798632d64823659f4814 (diff) | |
enforcing Ltac2 constructor name are uppercased
| -rw-r--r-- | user-contrib/Ltac2/tac2entries.ml | 7 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2env.ml | 7 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2env.mli | 1 |
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 |