From 1705c26e355620be3f249b4953c03b513846f3c2 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 12 Nov 2008 11:12:23 +0000
Subject: Les signatures des applications de foncteur sont précalculées, cela
 alourdit un peu les vo mais accélère la compilation lorsque les foncteurs
 sont massivement utilisés.

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

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index f4f52d83dd..cd93f4851b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -258,11 +258,13 @@ and translate_module env me =
     | Some mexpr, _ -> 
 	let meb,sub1 = translate_struct_entry env mexpr in
 	let mod_typ,sub,cst =
-	  match me.mod_entry_type with
-	    | None ->  
+	  match me.mod_entry_type,meb with
+	    | None,SEBapply _ ->
+		Some (eval_struct env meb),sub1,Constraint.empty
+	    | None,_ ->  
 		(type_of_struct env (bounded_str_expr meb) meb)
 		  ,sub1,Constraint.empty
-	    | Some mte -> 
+	    | Some mte,_ -> 
 		let mtb2,sub2 = translate_struct_entry env mte in
                 let cst = check_subtypes env
 		  {typ_expr = meb;
-- 
cgit v1.2.3