diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-01-19 22:34:29 +0000 |
| commit | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (patch) | |
| tree | fbb91e2f74c73bb867ab62c58f248a704bbe6dec /library/declaremods.ml | |
| parent | 6497f27021fec4e01f2182014f2bb1989b4707f9 (diff) | |
Imported Upstream version 8.0pl3upstream/8.0pl3
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index b968a432..2e8fb0a7 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.ml,v 1.18.2.1 2004/07/16 19:30:35 herbelin Exp $ i*) +(*i $Id: declaremods.ml,v 1.18.2.2 2005/12/30 11:08:56 herbelin Exp $ i*) open Pp open Util @@ -502,17 +502,17 @@ let end_module id = let dir = fst oldprefix in let msid = msid_of_prefix oldprefix in - let substobjs = try + let substobjs, keep, special = try match res_o with | None -> - empty_subst, mbids, msid, substitute + (empty_subst, mbids, msid, substitute), keep, special | Some (MTEident ln) -> - abstract_substobjs mbids (KNmap.find ln (!modtypetab)) + abstract_substobjs mbids (KNmap.find ln (!modtypetab)), [], [] | Some (MTEsig (msid,_)) -> todo "Anonymous signatures not supported"; - empty_subst, mbids, msid, [] + (empty_subst, mbids, msid, []), keep, special | Some (MTEwith _ as mty) -> - abstract_substobjs mbids (get_modtype_substobjs mty) + abstract_substobjs mbids (get_modtype_substobjs mty), [], [] | Some (MTEfunsig _) -> anomaly "Funsig cannot be here..." with |