From 2ad7d4704ae79f58a8bab0e190ab6e96b81831c3 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 15 Sep 2010 12:21:57 +0000
Subject: Sharing is not anymore broken by traverse_module. +commit r13412

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13418 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 checker/mod_checking.ml |  6 +++---
 checker/safe_typing.ml  | 21 +++++++++++++++++----
 kernel/safe_typing.ml   | 21 +++++++++++++++++----
 3 files changed, 37 insertions(+), 11 deletions(-)

diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 23ba4893a0..81154cba89 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -238,15 +238,15 @@ 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 in ()
+  let _ = 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 in ()
+	let _ = 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 in ()
+	let _ = 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
diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 70eccf9520..83364aa728 100644
--- a/checker/safe_typing.ml
+++ b/checker/safe_typing.ml
@@ -98,10 +98,23 @@ end = struct
      the opaque term [t] to [on_opaque_const_body t]. *)
   let traverse_library on_opaque_const_body =
     let rec traverse_module mb =
-      { mb with
-	mod_expr = Option.map traverse_modexpr mb.mod_expr;
-	mod_type = traverse_modexpr mb.mod_type;
-      }
+      match mb.mod_expr with 
+	  None -> 
+	    { mb with
+		mod_expr = None;
+		mod_type = traverse_modexpr mb.mod_type;
+	    }
+	| Some impl when impl == mb.mod_type-> 
+	    let mtb =  traverse_modexpr mb.mod_type in 
+	      { mb with
+		  mod_expr = Some mtb;
+		  mod_type = mtb;
+	      }    
+	| Some impl -> 
+	    { mb with
+		mod_expr = Option.map traverse_modexpr mb.mod_expr;
+		mod_type = traverse_modexpr mb.mod_type;
+	    }    
     and traverse_struct struc =
       let traverse_body (l,body) = (l,match body with
 	| SFBconst ({const_opaque=true} as x) -> 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2227142178..517a9c8099 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -865,10 +865,23 @@ end = struct
      the opaque term [t] to [on_opaque_const_body t]. *)
   let traverse_library on_opaque_const_body =
     let rec traverse_module mb =
-      { mb with
-	mod_expr = Option.map traverse_modexpr mb.mod_expr;
-	mod_type = traverse_modexpr mb.mod_type;
-      }
+      match mb.mod_expr with 
+	  None -> 
+	    { mb with
+		mod_expr = None;
+		mod_type = traverse_modexpr mb.mod_type;
+	    }
+	| Some impl when impl == mb.mod_type-> 
+	    let mtb =  traverse_modexpr mb.mod_type in 
+	      { mb with
+		  mod_expr = Some mtb;
+		  mod_type = mtb;
+	      }    
+	| Some impl -> 
+	    { mb with
+		mod_expr = Option.map traverse_modexpr mb.mod_expr;
+		mod_type = traverse_modexpr mb.mod_type;
+	    }    
     and traverse_struct struc =
       let traverse_body (l,body) = (l,match body with
 	| SFBconst ({const_opaque=true} as x) -> 
-- 
cgit v1.2.3