From 987b1ff5edb3fd0a694163ca46521d35466c7ea8 Mon Sep 17 00:00:00 2001
From: soubiran
Date: Thu, 3 Apr 2008 09:24:34 +0000
Subject: Patch sur le typage d'un foncteur applique a un alias.

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

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 36ef0c5e65..1b2147d286 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -245,12 +245,12 @@ and translate_struct_entry env mse = match mse with
       let farg_id, farg_b, fbody_b = destr_functor env feb' in
       let mtb,mp = 
 	try
-	  let mp = path_of_mexpr mexpr in
+	  let mp = scrape_alias (path_of_mexpr mexpr) env in
 	  lookup_modtype mp env,mp
 	with
 	  | Not_path -> error_application_to_not_path mexpr
 	      (* place for nondep_supertype *) in
-      let meb,sub2= translate_struct_entry env mexpr in
+      let meb,sub2= translate_struct_entry env (MSEident mp) in
       let sub2 = match eval_struct env (SEBident mp) with
 	| SEBstruct (msid,sign) -> subst_key (map_msid msid mp) sub2
 	| _ -> sub2 in
-- 
cgit v1.2.3