From 48d92bcbdc9fc4a967d6246d404e224aec448a28 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Fri, 14 Nov 2008 13:10:38 +0000
Subject: retour sur le commit 11579 qui faisait plante les contribs FSet et
 color.

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

(limited to 'kernel')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index cd93f4851b..f4f52d83dd 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -258,13 +258,11 @@ 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,meb with
-	    | None,SEBapply _ ->
-		Some (eval_struct env meb),sub1,Constraint.empty
-	    | None,_ ->  
+	  match me.mod_entry_type with
+	    | 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