diff options
| author | Pierre-Marie Pédrot | 2017-09-01 00:27:35 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-01 00:27:35 +0200 |
| commit | 1f7a2ea0e0513620bb946c10923d38f845061afa (patch) | |
| tree | 862ba03ff2dd5ee0b55aa807062afcde0b3c9c27 | |
| parent | 2a0a48834f0b90319e56ae9f4a172fe6855583c0 (diff) | |
Ensuring the Ltac definitions have lowercase names.
| -rw-r--r-- | src/tac2entries.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/tac2entries.ml b/src/tac2entries.ml index 2895fda060..efdc995a69 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -307,6 +307,10 @@ let inline_rec_tactic tactics = in List.map map tactics +let check_lowercase (loc, id) = + if Tac2env.is_constructor (Libnames.qualid_of_ident id) then + user_err ?loc (str "The identifier " ++ Id.print id ++ str " must be lowercase") + let register_ltac ?(local = false) ?(mut = false) isrec tactics = let map ((loc, na), e) = let id = match na with @@ -314,6 +318,7 @@ let register_ltac ?(local = false) ?(mut = false) isrec tactics = user_err ?loc (str "Tactic definition must have a name") | Name id -> id in + let () = check_lowercase (loc, id) in ((loc, id), e) in let tactics = List.map map tactics in @@ -648,8 +653,9 @@ let inTac2Abbreviation : abbreviation -> obj = classify_function = classify_abbreviation} let register_notation ?(local = false) tkn lev body = match tkn, lev with -| [SexprRec (_, (_, Some id), [])], None -> +| [SexprRec (_, (loc, Some id), [])], None -> (** Tactic abbreviation *) + let () = check_lowercase (loc, id) in let body = Tac2intern.globalize Id.Set.empty body in let abbr = { abbr_body = body } in ignore (Lib.add_leaf id (inTac2Abbreviation abbr)) |