From a16cb490545789ad0071d751ff9fbd149c55075d Mon Sep 17 00:00:00 2001
From: Vincent Laporte
Date: Mon, 5 Nov 2018 13:41:01 +0000
Subject: [Goptions] More detailed error messages

---
 library/goptions.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/goptions.ml b/library/goptions.ml
index dcbc46ab72..154b863fa1 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -73,7 +73,7 @@ module MakeTable =
 
     let _ =
       if String.List.mem_assoc nick !A.table then
-	user_err Pp.(str "Sorry, this table name is already used.")
+        user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.")
 
     module MySet = Set.Make (struct type t = A.t let compare = A.compare end)
 
@@ -216,11 +216,11 @@ let get_option key = OptionMap.find key !value_tab
 
 let check_key key = try
   let _ = get_option key in
-  user_err Pp.(str "Sorry, this option name is already used.")
+  user_err Pp.(str "Sorry, this option name ("++ str (nickname key) ++ str ") is already used.")
 with Not_found ->
   if String.List.mem_assoc (nickname key) !string_table
     || String.List.mem_assoc (nickname key) !ref_table
-  then user_err Pp.(str "Sorry, this option name is already used.")
+  then user_err Pp.(str "Sorry, this option name (" ++ str (nickname key) ++ str ") is already used.")
 
 open Libobject
 
-- 
cgit v1.2.3