diff options
| author | Pierre-Marie Pédrot | 2019-12-19 18:03:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-12-22 14:04:01 +0100 |
| commit | fcd903c299db00d5c8d3e2fa797404eb880b61ac (patch) | |
| tree | d1d339cb530d2f8e0c4afd11f49fb810383eb5ec /parsing/pcoq.ml | |
| parent | 9c75b6a6582620e2fb9a39c1ea1aa46a321af6a7 (diff) | |
Ensure that a custom entry cannot be defined twice.
This highlights the fact that diamond inheritance of a custom entry
is a tricky problem, as well as merely importing two custom entries with
the same name from two different modules. The only sane way to give a
semantics to that is to stick to module-scoped objects, i.e. give those
entries a kernel name. In the meantime, I went for a warning when
overriding entries.
Diffstat (limited to 'parsing/pcoq.ml')
| -rw-r--r-- | parsing/pcoq.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 734dd8ee8a..26afdcb9d5 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -533,6 +533,7 @@ let extend_entry_command (type a) (type b) (tag : (a, b) entry_command) (g : a) try EntryDataMap.find tag !camlp5_entries with Not_found -> EntryData.Ex String.Map.empty in + let () = assert (not @@ String.Map.mem name old) in let entries = String.Map.add name e old in camlp5_entries := EntryDataMap.add tag (EntryData.Ex entries) !camlp5_entries in |