From 1ffb37b4651dcc7a2b1d59285e07ea9e2a3febe5 Mon Sep 17 00:00:00 2001 From: glondu Date: Thu, 20 Oct 2011 05:47:47 +0000 Subject: More descriptive error messages in checker git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14576 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/environ.ml | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) (limited to 'checker/environ.ml') 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 -- cgit v1.2.3