From fcd903c299db00d5c8d3e2fa797404eb880b61ac Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 19 Dec 2019 18:03:34 +0100
Subject: 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.
---
 parsing/pcoq.ml                   |  1 +
 test-suite/success/custom_entry.v | 13 +++++++++++++
 vernac/egramcoq.ml                |  4 ++++
 vernac/egramcoq.mli               |  3 +++
 vernac/metasyntax.ml              | 13 +++++++++++--
 5 files changed, 32 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/success/custom_entry.v

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
diff --git a/test-suite/success/custom_entry.v b/test-suite/success/custom_entry.v
new file mode 100644
index 0000000000..e88ae65e18
--- /dev/null
+++ b/test-suite/success/custom_entry.v
@@ -0,0 +1,13 @@
+Declare Custom Entry foo.
+
+Print Custom Grammar foo.
+
+Notation "[ e ]" := e (e custom foo at level 0).
+
+Print Custom Grammar foo.
+
+Notation "1" := O (in custom foo at level 0).
+
+Print Custom Grammar foo.
+
+Fail Declare Custom Entry foo.
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index b65a126f55..07656f9715 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -278,6 +278,10 @@ let find_custom_entry s =
   try (find_custom_entry constr_custom_entry sc, find_custom_entry pattern_custom_entry sp)
   with Not_found -> user_err Pp.(str "Undeclared custom entry: " ++ str s ++ str ".")
 
+let exists_custom_entry s = match find_custom_entry s with
+| _ -> true
+| exception _ -> false
+
 let locality_of_custom_entry s = String.Set.mem s !custom_entry_locality
 
 (* This computes the name of the level where to add a new rule *)
diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli
index f879d51660..6768d24d5c 100644
--- a/vernac/egramcoq.mli
+++ b/vernac/egramcoq.mli
@@ -19,4 +19,7 @@ val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
 
 val create_custom_entry : local:bool -> string -> unit
+
+val exists_custom_entry : string -> bool
+
 val locality_of_custom_entry : string -> bool
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))
-- 
cgit v1.2.3