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.
---
 vernac/metasyntax.ml | 13 +++++++++++--
 1 file changed, 11 insertions(+), 2 deletions(-)

(limited to 'vernac/metasyntax.ml')

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