From f1686dbcad2515eee22b26b156fe51f6e9d22857 Mon Sep 17 00:00:00 2001 From: barras Date: Mon, 23 May 2011 15:06:48 +0000 Subject: ported r14149 from v8.3 branch: bug in checker (redefined global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14150 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/environ.ml | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'checker/environ.ml') diff --git a/checker/environ.ml b/checker/environ.ml index d79cb118b..7ba59d12a 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -111,6 +111,8 @@ let lookup_constant kn env = Cmap_env.find kn env.env_globals.env_constants let add_constant kn cs env = + if Cmap_env.mem kn env.env_globals.env_constants then + anomaly "Constant is already defined"; let new_constants = Cmap_env.add kn cs env.env_globals.env_constants in let new_globals = @@ -150,6 +152,8 @@ let lookup_mind kn env = Mindmap_env.find kn env.env_globals.env_inductives let add_mind kn mib env = + if Mindmap_env.mem kn env.env_globals.env_inductives then + anomaly "Inductive is already defined"; 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 @@ -166,6 +170,8 @@ let add_mind kn mib env = (* Modules *) let add_modtype ln mtb env = + if MPmap.mem ln env.env_globals.env_modtypes then + anomaly "Module type is already defined"; let new_modtypes = MPmap.add ln mtb env.env_globals.env_modtypes in let new_globals = { env.env_globals with @@ -173,6 +179,8 @@ let add_modtype ln mtb env = { env with env_globals = new_globals } let shallow_add_module mp mb env = + if MPmap.mem mp env.env_globals.env_modules then + anomaly "Module is already defined"; let new_mods = MPmap.add mp mb env.env_globals.env_modules in let new_globals = { env.env_globals with -- cgit v1.2.3