Imported Upstream version 8.3.pl3upstream/8.3.pl3

27 files changed, 118 insertions, 96 deletions

diff --git a/checker/check.ml b/checker/check.ml
index 9343d0b3..40119a7e 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/check_stat.ml b/checker/check_stat.ml
index 7ca406fe..88f2374b 100644
--- a/checker/check_stat.ml
+++ b/checker/check_stat.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/check_stat.mli b/checker/check_stat.mli
index 353edda6..d39eb454 100644
--- a/checker/check_stat.mli
+++ b/checker/check_stat.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/checker.ml b/checker/checker.ml
index 251197a1..76f81264 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/closure.ml b/checker/closure.ml
index 00ef6911..da25b3b3 100644
--- a/checker/closure.ml
+++ b/checker/closure.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/closure.mli b/checker/closure.mli
index fc147979..12cee770 100644
--- a/checker/closure.mli
+++ b/checker/closure.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/environ.ml b/checker/environ.ml
index a72aae91..f7dd46f8 100644
--- a/checker/environ.ml
+++ b/checker/environ.ml
@@ -111,6 +111,9 @@ 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
+    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 =
@@ -159,6 +162,9 @@ 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
+    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 
@@ -175,6 +181,9 @@ let add_mind kn mib env =
 (* Modules *)
 
 let add_modtype ln mtb env =
+  if MPmap.mem ln env.env_globals.env_modtypes then
+    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
@@ -182,12 +191,24 @@ 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
+    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
 	env_modules = new_mods } in
   { env with env_globals = new_globals }
 
+let shallow_remove_module mp env =
+  if not (MPmap.mem mp env.env_globals.env_modules) then
+    Printf.ksprintf anomaly "Module %s is unknown"
+      (string_of_mp mp);
+  let new_mods = MPmap.remove mp env.env_globals.env_modules in
+  let new_globals =
+    { env.env_globals with
+	env_modules = new_mods } in
+  { env with env_globals = new_globals }
 
 let lookup_module mp env =
   MPmap.find mp env.env_globals.env_modules
diff --git a/checker/environ.mli b/checker/environ.mli
index 023acd0b..ea446cdb 100644
--- a/checker/environ.mli
+++ b/checker/environ.mli
@@ -71,5 +71,6 @@ val add_modtype :
   module_path -> Declarations.module_type_body -> env -> env
 val shallow_add_module :
   module_path -> Declarations.module_body -> env -> env
+val shallow_remove_module : module_path -> env -> env
 val lookup_module : module_path -> env -> Declarations.module_body
 val lookup_modtype : module_path -> env -> Declarations.module_type_body
diff --git a/checker/indtypes.ml b/checker/indtypes.ml
index 2431f14e..277fed30 100644
--- a/checker/indtypes.ml
+++ b/checker/indtypes.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/indtypes.mli b/checker/indtypes.mli
index 181237fc..bca0a643 100644
--- a/checker/indtypes.mli
+++ b/checker/indtypes.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/inductive.ml b/checker/inductive.ml
index fcd69f26..b9964fe6 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/inductive.mli b/checker/inductive.mli
index d44d1556..e658a798 100644
--- a/checker/inductive.mli
+++ b/checker/inductive.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 81154cba..95387cac 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -213,7 +213,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
@@ -238,30 +238,39 @@ 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
-          check_subtypes env 
-	    {typ_mp=mp;
-	     typ_expr=sign;
-	     typ_expr_alg=None;
-	     typ_constraints=Univ.Constraint.empty;
-	     typ_delta = mb.mod_delta;}
-	    {typ_mp=mp;
-	     typ_expr=mb.mod_type;
-	     typ_expr_alg=None;
-	     typ_constraints=Univ.Constraint.empty;
-	     typ_delta = mb.mod_delta;};
-	  
+	let (_:struct_expr_body) =
+	  check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in
+	let mtb1 =
+	  {typ_mp=mp;
+	   typ_expr=sign;
+	   typ_expr_alg=None;
+	   typ_constraints=Univ.Constraint.empty;
+	   typ_delta = mb.mod_delta;}
+	and mtb2 =
+	  {typ_mp=mp;
+	   typ_expr=mb.mod_type;
+	   typ_expr_alg=None;
+	   typ_constraints=Univ.Constraint.empty;
+	   typ_delta = mb.mod_delta;};
+	in
+	let env = add_module (module_body_of_type mp mtb1) env in
+	check_subtypes env mtb1 mtb2
+
 and check_structure_field env mp lab res = function
   | SFBconst cb ->
       let c = make_con mp empty_dirpath lab in
@@ -271,7 +280,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;
@@ -280,7 +289,7 @@ and check_structure_field env mp lab res = function
 and check_modexpr env mse mp_mse res = match mse with
   | SEBident mp ->
       let mb = lookup_module mp env in
-      	(subst_and_strengthen mb mp_mse env).mod_type
+      (subst_and_strengthen mb mp_mse).mod_type
   | SEBfunctor (arg_id, mtb, body) ->
       check_module_type env mtb ;
       let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
@@ -293,7 +302,7 @@ and check_modexpr env mse mp_mse res = match mse with
 	try (path_of_mexpr m)
 	with Not_path -> error_application_to_not_path m
 	  (* place for nondep_supertype *) in
-      let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+      let mtb = module_type_of_module (Some mp) (lookup_module mp env) in
 	check_subtypes env mtb farg_b;
 	(subst_struct_expr (map_mbid farg_id mp) fbody_b)
   | SEBwith(mte, with_decl) ->
@@ -301,7 +310,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)
 	
@@ -321,7 +330,7 @@ and check_modtype env mse mp_mse res = match mse with
 	try (path_of_mexpr m)
 	with Not_path -> error_application_to_not_path m
 	  (* place for nondep_supertype *) in
-      let mtb = module_type_of_module env (Some mp) (lookup_module mp env) in
+      let mtb = module_type_of_module (Some mp) (lookup_module mp env) in
 	check_subtypes env mtb farg_b;
 	subst_struct_expr (map_mbid farg_id mp) fbody_b
   | SEBwith(mte, with_decl) ->
@@ -329,7 +338,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)
 	
diff --git a/checker/modops.ml b/checker/modops.ml
index 6d53803b..38aeaee2 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -111,7 +111,7 @@ and add_module mb env =
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
 
-let strengthen_const env mp_from l cb resolver = 
+let strengthen_const mp_from l cb resolver =
   match cb.const_opaque, cb.const_body with
   | false, Some _ -> cb
   | true, Some _ 
@@ -126,14 +126,14 @@ let strengthen_const env mp_from l cb resolver =
 	}
 	  
 
-let rec strengthen_mod env mp_from mp_to mb = 
+let rec strengthen_mod mp_from mp_to mb =
   if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then
     mb 
   else
     match mb.mod_type with
      | SEBstruct (sign) -> 
 	 let resolve_out,sign_out = 
-	   strengthen_sig env mp_from sign mp_to mb.mod_delta in
+	   strengthen_sig mp_from sign mp_to mb.mod_delta in
 	   { mb with
 	       mod_expr = Some (SEBident mp_to);
 	       mod_type = SEBstruct(sign_out);
@@ -145,60 +145,49 @@ let rec strengthen_mod env mp_from mp_to mb =
      | SEBfunctor _ -> mb
      | _ -> anomaly "Modops:the evaluation of the structure failed "
 	 
-and strengthen_sig env mp_from sign mp_to resolver =
+and strengthen_sig mp_from sign mp_to resolver =
   match sign with
     | [] -> empty_delta_resolver,[]
     | (l,SFBconst cb) :: rest ->
-	let item' = 
-	  l,SFBconst (strengthen_const env mp_from l cb resolver) in
-	let resolve_out,rest' =
-	  strengthen_sig env mp_from rest mp_to resolver in
-	  resolve_out,item'::rest'
+	let item' = l,SFBconst (strengthen_const mp_from l cb resolver) in
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out,item'::rest'
     | (_,SFBmind _ as item):: rest ->
-	let resolve_out,rest' = 
-	  strengthen_sig env mp_from rest mp_to resolver in
-	  resolve_out,item::rest'
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out,item::rest'
     | (l,SFBmodule mb) :: rest ->
 	let mp_from' = MPdot (mp_from,l) in
-	let mp_to' = MPdot(mp_to,l) in 
-	let mb_out = 
-	  strengthen_mod env mp_from' mp_to' mb in
+	let mp_to' = MPdot(mp_to,l) in
+	let mb_out = strengthen_mod mp_from' mp_to' mb in
 	let item' = l,SFBmodule (mb_out) in
-	let env' = add_module mb_out env in
-	let resolve_out,rest' = 
-	  strengthen_sig env' mp_from rest mp_to resolver in
-	  resolve_out
-	  (*add_delta_resolver resolve_out mb.mod_delta*),
-	item':: rest'
-    | (l,SFBmodtype mty as item) :: rest -> 
-	let env' = add_modtype 
-	  (MPdot(mp_from,l)) mty env
-	in
-	let resolve_out,rest' = 
-	  strengthen_sig env' mp_from rest mp_to resolver in
-	  resolve_out,item::rest'
-    
-let strengthen env mtb mp = 
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out, item'::rest'
+    | (l,SFBmodtype mty as item) :: rest ->
+	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
+	resolve_out, item::rest'
+
+let strengthen mtb mp =
     match mtb.typ_expr with
-      | SEBstruct (sign) -> 
+      | SEBstruct (sign) ->
 	  let resolve_out,sign_out =
-	    strengthen_sig env mtb.typ_mp sign mp mtb.typ_delta in
-	    {mtb with
-	       typ_expr = SEBstruct(sign_out);
-	       typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
+	    strengthen_sig mtb.typ_mp sign mp mtb.typ_delta
+	  in
+	  {mtb with
+	    typ_expr = SEBstruct(sign_out);
+	    typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
 		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
       | SEBfunctor _ -> mtb
       | _ -> anomaly "Modops:the evaluation of the structure failed "
 
-let subst_and_strengthen mb mp env =
-  strengthen_mod env mb.mod_mp mp 
+let subst_and_strengthen mb mp =
+  strengthen_mod mb.mod_mp mp
     (subst_module (map_mp mb.mod_mp mp) mb)
 
 
-let module_type_of_module env mp mb =
+let module_type_of_module mp mb =
   match mp with
       Some mp ->
-	strengthen env {
+	strengthen {
 	  typ_mp = mp;
 	  typ_expr = mb.mod_type;
 	  typ_expr_alg = None;
diff --git a/checker/modops.mli b/checker/modops.mli
index b218b052..2f9f2e8c 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -22,7 +22,7 @@ open Environ
 (* make the envirconment entry out of type *)
 val module_body_of_type : module_path -> module_type_body -> module_body
 
-val module_type_of_module : env -> module_path option -> module_body ->
+val module_type_of_module : module_path option -> module_body ->
   module_type_body
 
 val destr_functor :
@@ -35,9 +35,9 @@ val add_module : module_body ->  env -> env
 
 val check_modpath_equiv : env -> module_path -> module_path -> unit
 
-val strengthen : env -> module_type_body -> module_path -> module_type_body
+val strengthen : module_type_body -> module_path -> module_type_body
 
-val subst_and_strengthen : module_body -> module_path -> env -> module_body 
+val subst_and_strengthen : module_body -> module_path -> module_body
 
 val error_incompatible_modtypes :
   module_type_body -> module_type_body -> 'a
diff --git a/checker/reduction.ml b/checker/reduction.ml
index d040c3db..ba8ceeef 100644
--- a/checker/reduction.ml
+++ b/checker/reduction.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/reduction.mli b/checker/reduction.mli
index 0d65daa4..8e69da44 100644
--- a/checker/reduction.mli
+++ b/checker/reduction.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 07718a09..a669c5e8 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/safe_typing.mli b/checker/safe_typing.mli
index 154634c5..00aa1a84 100644
--- a/checker/safe_typing.mli
+++ b/checker/safe_typing.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 684a59ad..4f113cf9 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -280,8 +280,8 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 =
    | _ -> error ()
 
 let rec check_modules  env msb1 msb2 subst1 subst2 =
-  let mty1 = module_type_of_module env None msb1 in
-  let mty2 =  module_type_of_module env None msb2 in
+  let mty1 = module_type_of_module None msb1 in
+  let mty2 =  module_type_of_module None msb2 in
     check_modtypes env mty1 mty2 subst1 subst2 false;
  
 
@@ -343,7 +343,8 @@ and check_modtypes  env mtb1 mtb2 subst1 subst2 equiv =
 		(module_body_of_type (MPbound arg_id2) arg_t2) env 
 	      in
 	      let env = match body_t1 with
-		  SEBstruct str -> 
+		  SEBstruct str ->
+		    let env = shallow_remove_module mtb1.typ_mp env in
 		    add_module {mod_mp = mtb1.typ_mp;
 				mod_expr = None;
 				mod_type = body_t1;
@@ -363,10 +364,8 @@ and check_modtypes  env mtb1 mtb2 subst1 subst2 equiv =
 
 let check_subtypes env sup super =
   (*if sup<>super then*)
-  let env = add_module 
-    (module_body_of_type sup.typ_mp sup) env in
-    check_modtypes env (strengthen env sup sup.typ_mp) super empty_subst 
-      (map_mp super.typ_mp sup.typ_mp) false 
+  check_modtypes env (strengthen sup sup.typ_mp) super empty_subst
+    (map_mp super.typ_mp sup.typ_mp) false
 
 let check_equal env sup super =
   (*if sup<>super then*)
diff --git a/checker/subtyping.mli b/checker/subtyping.mli
index d88ee0b2..d9cbe5ad 100644
--- a/checker/subtyping.mli
+++ b/checker/subtyping.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -15,6 +15,9 @@ open Declarations
 open Environ
 (*i*)
 
+(** Invariant: the first [module_type_body] is now supposed to be
+    known by [env] *)
+
 val check_subtypes : env -> module_type_body -> module_type_body -> unit
 val check_equal : env -> module_type_body -> module_type_body -> unit
 
diff --git a/checker/term.ml b/checker/term.ml
index f472f994..61369586 100644
--- a/checker/term.ml
+++ b/checker/term.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/type_errors.ml b/checker/type_errors.ml
index a94f3988..bd3bb90d 100644
--- a/checker/type_errors.ml
+++ b/checker/type_errors.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/type_errors.mli b/checker/type_errors.mli
index 8ca19ddc..82cb3c55 100644
--- a/checker/type_errors.mli
+++ b/checker/type_errors.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/typeops.ml b/checker/typeops.ml
index c04586b3..dffc9fe1 100644
--- a/checker/typeops.ml
+++ b/checker/typeops.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/typeops.mli b/checker/typeops.mli
index 08ef433f..f4f29fe5 100644
--- a/checker/typeops.mli
+++ b/checker/typeops.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/checker/validate.ml b/checker/validate.ml
index 688a1319..7d368f05 100644
--- a/checker/validate.ml
+++ b/checker/validate.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)