diff options
| author | Hugo Herbelin | 2019-12-27 13:30:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-27 13:30:49 +0100 |
| commit | 9c74438f09c2dddaa320eccf4d0842c77e3c863d (patch) | |
| tree | 53a3b812bd8c08715e3a9f7b77681f4eb3d51fef /vernac/metasyntax.ml | |
| parent | 4c19baf3a1b0ee9b1e94df4bca29c53125445db8 (diff) | |
| parent | fcd903c299db00d5c8d3e2fa797404eb880b61ac (diff) | |
Merge PR #11315: Ensure that a custom entry cannot be defined twice.
Reviewed-by: herbelin
Reviewed-by: maximedenes
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 35681aed13..222e9eb825 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1654,10 +1654,16 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing (**********************************************************************) (* Declaration of custom entry *) +let warn_custom_entry = + CWarnings.create ~name:"custom-entry-overriden" ~category:"parsing" + (fun s -> + strbrk "Custom entry " ++ str s ++ strbrk " has been overriden.") + let load_custom_entry _ _ = () let open_custom_entry _ (_,(local,s)) = - Egramcoq.create_custom_entry ~local s + if Egramcoq.exists_custom_entry s then warn_custom_entry s + else Egramcoq.create_custom_entry ~local s let cache_custom_entry o = load_custom_entry 1 o; @@ -1677,4 +1683,7 @@ let inCustomEntry : locality_flag * string -> obj = classify_function = classify_custom_entry} let declare_custom_entry local s = - Lib.add_anonymous_leaf (inCustomEntry (local,s)) + if Egramcoq.exists_custom_entry s then + user_err Pp.(str "Custom entry " ++ str s ++ str " already exists") + else + Lib.add_anonymous_leaf (inCustomEntry (local,s)) |