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

2 files changed, 21 insertions, 8 deletions

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
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 285039eae..315571705 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -211,7 +211,7 @@ and check_with_aux_mod env mtb with_decl mp =
 		  SFBmodule msb -> msb
 		| _ -> error_not_a_module l
 	      in
-	      let _ = (lookup_module mp1 env) in ()
+	      let (_:module_body) = (lookup_module mp1 env) in ()
         | With_module_body (_::_,mp) ->
 	    let old = match spec with
 		SFBmodule msb -> msb
@@ -236,18 +236,23 @@ and check_with_aux_mod env mtb with_decl mp =
       | Reduction.NotConvertible -> error_with_incorrect l
 
 and check_module_type env mty =
-  let _ = check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in ()
+  let (_:struct_expr_body) =
+    check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in
+  ()
 
 							 
 and check_module env mp mb =
   match mb.mod_expr, mb.mod_type with
     | None,mtb -> 
-	let _ = check_modtype env mtb mb.mod_mp mb.mod_delta in ()
+	let (_:struct_expr_body) =
+	  check_modtype env mtb mb.mod_mp mb.mod_delta in ()
     | Some mexpr, mtb when mtb==mexpr ->
-	let _ = check_modtype env mtb mb.mod_mp mb.mod_delta in ()
+	let (_:struct_expr_body) =
+	  check_modtype env mtb mb.mod_mp mb.mod_delta in ()
     | Some mexpr, _ ->
 	let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in
-	let _ = check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in
+	let (_:struct_expr_body) =
+	  check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in
           check_subtypes env 
 	    {typ_mp=mp;
 	     typ_expr=sign;
@@ -269,7 +274,7 @@ and check_structure_field env mp lab res = function
       let kn = mind_of_delta res kn in
 	Indtypes.check_inductive env kn mib
   | SFBmodule msb ->
-      let _= check_module env (MPdot(mp,lab)) msb in
+      let (_:unit) = check_module env (MPdot(mp,lab)) msb in
 	Modops.add_module msb env
   | SFBmodtype mty ->
       check_module_type env mty;
@@ -299,7 +304,7 @@ and check_modexpr env mse mp_mse res = match mse with
       let sign = check_with env sign with_decl mp_mse in 
 	sign
   | SEBstruct(msb) ->
-      let _ = List.fold_left (fun env (lab,mb) ->
+      let (_:env) = List.fold_left (fun env (lab,mb) ->
 		   check_structure_field env mp_mse lab res mb) env msb in
 	SEBstruct(msb)
 	
@@ -327,7 +332,7 @@ and check_modtype env mse mp_mse res = match mse with
       let sign = check_with env sign with_decl mp_mse in
 	sign
   | SEBstruct(msb) ->
-      let _ = List.fold_left (fun env (lab,mb) ->
+      let (_:env) = List.fold_left (fun env (lab,mb) ->
 		   check_structure_field env mp_mse lab res mb) env msb in
       SEBstruct(msb)