From eb26bfab9ed53d981859bea5208595cd921ff42d Mon Sep 17 00:00:00 2001
From: regisgia
Date: Fri, 27 Aug 2010 12:41:26 +0000
Subject: * (checker|kernel)/Safe_typing:   Fix a bug in traverse_library.  
 The extraction was not satisfied with [mod_expr] set to [None].

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13384 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/safe_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 504bfab04b..43090c8e10 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -866,7 +866,7 @@ end = struct
   let traverse_library on_opaque_const_body =
     let rec lighten_module mb =
       { mb with
-	mod_expr = None;
+	mod_expr = Option.map lighten_modexpr mb.mod_expr;
 	mod_type = lighten_modexpr mb.mod_type;
       }
     and lighten_struct struc =
-- 
cgit v1.2.3