diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-03 09:24:34 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-03 09:24:34 +0000 |
| commit | 987b1ff5edb3fd0a694163ca46521d35466c7ea8 (patch) | |
| tree | 22d4cfa5a9aa386846ae489ec88a0eff96b3967e | |
| parent | 6e2ca58652b23415cba082c4be77823f182d14ba (diff) | |
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
| -rw-r--r-- | kernel/mod_typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 36ef0c5e6..1b2147d28 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 |