From b1eef69751a05eebdbdc9d3091e1dae3386218d0 Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 16 Aug 2002 10:00:36 +0000
Subject: Strengthenning rules for modules + No modules in sections

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/mod_typing.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 5c4b00d94f..1eb74ffef6 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -32,6 +32,8 @@ let rec list_fold_map2 f e = function
        let e'',t1',t2' = list_fold_map2 f e' t in
 	 e'',h1'::t1',h2'::t2'
 
+let type_modpath env mp = 
+  strengthen env (lookup_module mp env).mod_type mp
 
 let rec translate_modtype env mte =
   match mte with
@@ -100,7 +102,7 @@ and translate_module env is_definition me =
 	      with 
 		| Not_path -> error_declaration_not_path mexpr
 	    in
-	      MEBident mp, (lookup_module mp env).mod_type
+	      MEBident mp, type_modpath env mp
 	in
 	let mtb,mod_user_type =
 	  match me.mod_entry_type with
@@ -118,7 +120,7 @@ and translate_module env is_definition me =
 and translate_mexpr env mexpr = match mexpr with
   | MEident mp -> 
       MEBident mp,
-      (lookup_module mp env).mod_type
+      type_modpath env mp
   | MEfunctor (arg_id, arg_e, body_expr) ->
       let arg_b = translate_modtype env arg_e in
       let env' = add_module (MPbound arg_id) (module_body_of_type arg_b) env in
-- 
cgit v1.2.3