More descriptive error messages in checker

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14576 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 8 insertions, 4 deletions

diff --git a/checker/environ.ml b/checker/environ.ml
index 7ba59d12a..fbe9d9ee2 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -112,7 +112,8 @@ let lookup_constant kn env =
 
 let add_constant kn cs env =
   if Cmap_env.mem kn env.env_globals.env_constants then
-    anomaly "Constant is already defined";
+    Printf.ksprintf anomaly "Constant %s is already defined"
+      (string_of_con kn);
   let new_constants =
     Cmap_env.add kn cs env.env_globals.env_constants in
   let new_globals =
@@ -153,7 +154,8 @@ let lookup_mind kn env =
 
 let add_mind kn mib env =
   if Mindmap_env.mem kn env.env_globals.env_inductives then
-    anomaly "Inductive is already defined";
+    Printf.ksprintf anomaly "Inductive %s is already defined"
+      (string_of_mind kn);
   let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in
   let kn1,kn2 =  user_mind kn,canonical_mind kn in
   let new_inds_eq = if kn1=kn2 then 
@@ -171,7 +173,8 @@ let add_mind kn mib env =
 
 let add_modtype ln mtb env =
   if MPmap.mem ln env.env_globals.env_modtypes then
-    anomaly "Module type is already defined";
+    Printf.ksprintf anomaly "Module type %s is already defined"
+      (string_of_mp ln);
   let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in
   let new_globals =
     { env.env_globals with
@@ -180,7 +183,8 @@ let add_modtype ln mtb env =
 
 let shallow_add_module mp mb env =
   if MPmap.mem mp env.env_globals.env_modules then
-    anomaly "Module is already defined";
+    Printf.ksprintf anomaly "Module %s is already defined"
+      (string_of_mp mp);
   let new_mods = MPmap.add mp mb env.env_globals.env_modules in
   let new_globals =
     { env.env_globals with