diff options
| author | soubiran | 2008-04-23 11:51:44 +0000 |
|---|---|---|
| committer | soubiran | 2008-04-23 11:51:44 +0000 |
| commit | 2100f292ee109f9a75eb9d79c2234846d7135755 (patch) | |
| tree | f58fc977d89bdad14e90b207f195c4b5966a103f /kernel | |
| parent | ee4c7b812c9a2eefbf44097f9168ca1c55c2e668 (diff) | |
correction du bug sur Parameter Inline que j'ai reouvert hier par inadvertance
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10837 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/modops.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 0d0af00f09..590db27274 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -263,11 +263,11 @@ let rec eval_struct env = function (subst_key (map_msid msid mp) sub_alias) (map_msid msid mp) | _ -> sub_alias in - let sub_alias = update_subst_alias sub_alias + let sub_alias1 = update_subst_alias sub_alias (map_mbid farg_id mp (None)) in let resolve = resolver_of_environment farg_id farg_b mp sub_alias env in eval_struct env (subst_struct_expr - (join sub_alias + (join sub_alias1 (map_mbid farg_id mp (Some resolve))) fbody_b) | SEBwith (mtb,(With_definition_body _ as wdb)) -> let mtb',_ = merge_with env mtb wdb empty_subst in @@ -437,8 +437,9 @@ and resolver_of_environment mbid modtype mp alias env = let rec make_resolve = function | [] -> [] | (con,expecteddef)::r -> - let con',_ = subst_con alias con in - let con' = replace_mp_in_con (MPbound mbid) mp con' in + let con' = replace_mp_in_con (MPbound mbid) mp con in + let con',_ = subst_con alias con' in + (* let con' = replace_mp_in_con (MPbound mbid) mp con' in *) try if expecteddef.Declarations.const_inline then let constant = lookup_constant con' env in |