diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-25 15:55:16 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-25 15:55:16 +0000 |
| commit | a4bd836942106154703e10805405e8b4e6eb11ee (patch) | |
| tree | 704e5ab788a7d9d27b85828a89c43705741d6e79 /kernel/mod_typing.ml | |
| parent | 166714d89845f7e2f894fcd0fd92ae16961ca9eb (diff) | |
correction bug 1839
is line, and those below, will be ignored--
M kernel/mod_subst.mli
M kernel/mod_typing.ml
M kernel/mod_subst.ml
M kernel/subtyping.ml
M kernel/modops.ml
M library/declaremods.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10849 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/mod_typing.ml')
| -rw-r--r-- | kernel/mod_typing.ml | 30 |
1 files changed, 14 insertions, 16 deletions
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 09edc63f6..4a2dd9afc 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -263,27 +263,25 @@ and translate_struct_entry env mse = match mse with | Not_path -> error_application_to_not_path mexpr (* place for nondep_supertype *) 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 - let sub3= - if sub1 = empty_subst then - update_subst_alias sub2 (map_mbid farg_id mp None) + if sub1 = empty_subst then + let cst = check_subtypes env mtb farg_b in + SEBapply(feb,meb,cst),sub1 else - update_subst_alias sub2 - (join_alias sub1 (map_mbid farg_id mp None)) - in - let sub = if sub2 = sub3 then - join sub1 sub2 else join (join sub1 sub2) sub3 in - let sub = join_alias sub (map_mbid farg_id mp None) in - let sub = update_subst_alias sub (map_mbid farg_id mp None) in - let cst = check_subtypes env mtb farg_b in - SEBapply(feb,meb,cst),sub + let sub2 = match eval_struct env (SEBident mp) with + | SEBstruct (msid,sign) -> + join_alias + (subst_key (map_msid msid mp) sub2) + (map_msid msid mp) + | _ -> sub2 in + let sub3 = join_alias sub1 (map_mbid farg_id mp None) in + let sub4 = update_subst sub2 sub3 in + let cst = check_subtypes env mtb farg_b in + SEBapply(feb,meb,cst),(join sub3 sub4) | MSEwith(mte, with_decl) -> let mtb,sub1 = translate_struct_entry env mte in let mtb',sub2 = check_with env mtb with_decl in mtb',join sub1 sub2 - + let rec add_struct_expr_constraints env = function | SEBident _ -> env |