diff options
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 |