diff options
| author |  soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-05 13:28:06 +0000 |
|---|---|---|
| committer | soubiran <soubiran@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-02-05 13:28:06 +0000 |
| commit | 44cedab7be5a44a01d467fbd2dba24400d575206 (patch) | |
| tree | b393715a7768e0aaef2b9248524663daac8d50c6 /library/declaremods.ml | |
| parent | 362ccc063fa14ee0dbec6f25f1d4c45eca11013a (diff) | |
Correction d'un bug sur les substitutions:
Require Import FSets FSetAVL.
Module M:=FSetAVL.Make Z_as_OT. (* ... uncaught exception Not_found *)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10509 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 44907fd58..dffdb9e6f 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -545,7 +545,7 @@ let rec get_modtype_substobjs env = function Modops.resolver_of_environment farg_id farg_b mp env in (* application outside the kernel, only for substitutive objects (that are all non-logical objects) *) - (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs) + (join subst (add_mbid mbid mp (Some resolve) empty_subst), mbids, msid, objs) | [] -> match mexpr with | MSEident _ -> error "Application of a non-functor" | _ -> error "Application of a functor with too few arguments") @@ -849,7 +849,7 @@ let rec get_module_substobjs env = function Modops.resolver_of_environment farg_id farg_b mp env in (* application outside the kernel, only for substitutive objects (that are all non-logical objects) *) - (add_mbid mbid mp (Some resolve) subst, mbids, msid, objs) + (join subst (add_mbid mbid mp (Some resolve) empty_subst), mbids, msid, objs) | [] -> match mexpr with | MSEident _ -> error "Application of a non-functor" | _ -> error "Application of a functor with too few arguments") |