diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-13 14:07:29 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-13 14:07:29 +0000 |
| commit | 697b0f15cac660ea044ac8226c8e09e1d2cdb064 (patch) | |
| tree | ee1586587f5078bc4011a2457ca67f6e2a07b8be /kernel | |
| parent | 6832bab205c662c79e95431f50acad03c5940986 (diff) | |
Bug 2050, commit v8.2 11923-11924 ---> trunk
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11925 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/mod_subst.ml | 12 | ||||
| -rw-r--r-- | kernel/modops.ml | 6 |
2 files changed, 9 insertions, 9 deletions
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 040d7f811..2ac7b623b 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -356,23 +356,23 @@ let update_subst subst1 subst2 = | MPI mp -> mp in match mp with - | MPbound mbid -> ((MBI mbid),newmp)::l - | MPself msid -> ((MSI msid),newmp)::l - | _ -> ((MPI mp),newmp)::l + | MPbound mbid -> ((MBI mbid),newmp,resolve)::l + | MPself msid -> ((MSI msid),newmp,resolve)::l + | _ -> ((MPI mp),newmp,resolve)::l in let subst_mbi = Umap.fold subst_inv subst2 [] in let alias_subst key (mp,resolve) sub= let newsetkey = match key with | MPI mp1 -> - let compute_set_newkey l (k,mp') = + let compute_set_newkey l (k,mp',resolve) = let mp_from_key = match k with | MBI msid -> MPbound msid | MSI msid -> MPself msid | MPI mp -> mp in let new_mp1 = replace_mp_in_mp mp_from_key mp' mp1 in - if new_mp1 == mp1 then l else (MPI new_mp1)::l + if new_mp1 == mp1 then l else (MPI new_mp1,resolve)::l in begin match List.fold_left compute_set_newkey [] subst_mbi with @@ -384,7 +384,7 @@ let update_subst subst1 subst2 = match newsetkey with | None -> sub | Some l -> - List.fold_left (fun s k -> Umap.add k (mp,resolve) s) + List.fold_left (fun s (k,r) -> Umap.add k (mp,r) s) sub l in Umap.fold alias_subst subst1 empty_subst diff --git a/kernel/modops.ml b/kernel/modops.ml index f904bab54..8febff5e8 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -273,9 +273,9 @@ let rec eval_struct env = function (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in - let sub_alias1 = update_subst sub_alias - (map_mbid farg_id mp (None)) in - let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in + let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in + let sub_alias1 = update_subst sub_alias + (map_mbid farg_id mp (Some resolve)) in eval_struct env (subst_struct_expr (join sub_alias1 (map_mbid farg_id mp (Some resolve))) fbody_b) |