diff options
| author | soubiran | 2008-03-25 16:55:10 +0000 |
|---|---|---|
| committer | soubiran | 2008-03-25 16:55:10 +0000 |
| commit | 7dfb5d517e932b1b42445e4b1413dca72693cc4d (patch) | |
| tree | d3eff39598a905c31326ab82537b25a5e265b7ee /kernel/modops.ml | |
| parent | 36780f223b50549f522ac2832eab127a9cc40615 (diff) | |
Correction de bugs relatifs a la compostion des substitutions
engendrees par les alias de module
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10718 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index dc339af52e..8d74c4c300 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -271,6 +271,9 @@ let rec eval_struct env = function | SEBwith (mtb, (With_module_body (_,mp,_) as wdb)) -> let alias_in_mp = (lookup_modtype mp env).typ_alias in + let alias_in_mp = match eval_struct env (SEBident mp) with + | SEBstruct (msid,sign) -> subst_key (map_msid msid mp) alias_in_mp + | _ -> alias_in_mp in merge_with env mtb wdb alias_in_mp (* | SEBfunctor(mbid,mtb,body) -> let env = add_module (MPbound mbid) (module_body_of_type mtb) env in @@ -308,8 +311,9 @@ and merge_with env mtb with_decl alias= SFBconst c,None | With_module_body ([id], mp,cst) -> let mp' = scrape_alias mp env in + let new_alias = update_subst_alias alias (map_mp (mp_rec [id]) mp') in SFBalias (mp,Some cst), - Some(join (map_mp (mp_rec [id]) mp') alias) + Some(join (map_mp (mp_rec [id]) mp') new_alias) | With_definition_body (_::_,_) | With_module_body (_::_,_,_) -> let old = match spec with @@ -323,6 +327,9 @@ and merge_with env mtb with_decl alias= With_module_body (idl,mp,cst), Some(map_mp (mp_rec idc) mp) in + let subst1 = match subst1 with + | None -> None + | Some s -> Some (update_subst_alias alias s) in let subst = Option.fold_right join subst1 alias in let modtype = merge_with env (type_of_mb env old) new_with_decl alias in |