From 2ad7d4704ae79f58a8bab0e190ab6e96b81831c3 Mon Sep 17 00:00:00 2001
From: soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7>
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/safe_typing.ml | 21 +++++++++++++++++----
 1 file changed, 17 insertions(+), 4 deletions(-)

(limited to 'checker/safe_typing.ml')

diff --git a/checker/safe_typing.ml b/checker/safe_typing.ml
index 70eccf952..83364aa72 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) -> 
-- 
cgit v1.2.3