diff options
| author | soubiran | 2010-01-04 10:32:52 +0000 |
|---|---|---|
| committer | soubiran | 2010-01-04 10:32:52 +0000 |
| commit | f3979966ec7d1e5c13fd77e2d19856a3dd2e7a3f (patch) | |
| tree | a85d5f89f8ea1dd70899d0d807c9bf0e26d4b4e3 /kernel | |
| parent | 555c24b7c16a561eac480a64dff0856c8a4313a5 (diff) | |
The following script was rasing an error
Require Export FSets FMaps.
Require FMapAVL.
(* avl ou listes : aucun impact pour l'instant... *)
Module FMap := FMapList.
Module FMapHide (X : FMapInterface.S).
Include X.
End FMapHide.
Module State := Nat_as_OT.
Module StateMap' := FMap.Make(State). Module StateMap := FMapHide StateMap'.
Module LabelMap := StateMap.
About LabelMap.MapsTo. (*cannot print global_reference ....*)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12620 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/modops.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 2cc0f17ea9..8c014c1d7d 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -478,14 +478,14 @@ let strengthen_and_subst_mb mb mp env include_b = (i.e. it is already done)*) let mp_alias = delta_of_mp mb.mod_delta mb.mod_mp in let subst_resolver = map_mp mb.mod_mp mp empty_delta_resolver in - let resolver = + let new_resolver = add_mp_delta_resolver mp mp_alias (subst_dom_delta_resolver subst_resolver mb.mod_delta) in - let subst = map_mp mb.mod_mp mp resolver in + let subst = map_mp mb.mod_mp mp new_resolver in let resolver = if mb_is_an_alias && include_b then remove_mp_delta_resolver mb.mod_delta mb.mod_mp else mb.mod_delta in - let resolver,new_sig = + let resolver_out,new_sig = strengthen_and_subst_struct str subst env mp_alias mb.mod_mp mp mb_is_an_alias include_b resolver in @@ -493,8 +493,8 @@ let strengthen_and_subst_mb mb mp env include_b = mod_mp = mp; mod_type = SEBstruct(new_sig); mod_expr = Some (SEBident mb.mod_mp); - mod_delta = if include_b then resolver - else add_mp_delta_resolver mp mp_alias resolver} + mod_delta = if include_b then resolver_out + else add_delta_resolver new_resolver resolver_out} | SEBfunctor(arg_id,argb,body) -> let subst = map_mp mb.mod_mp mp empty_delta_resolver in subst_module subst |