diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-24 00:25:55 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-24 00:25:55 +0000 |
| commit | 7a367644e539a822be1bbb0d93742b915061cb15 (patch) | |
| tree | 0bd6c7db9406555cc66742185ba92ff4526db11f /library/declaremods.ml | |
| parent | bb98d8e44ca30c8db605aaccadfe74682914f6a0 (diff) | |
Tentative de réparation du bug #1025: it seems like that a casted module should only rely on the contents of its signature (i.e. with removal of the keep and special objects), doesn't it?
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7720 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index 250411e6b..b33b12d2b 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -509,17 +509,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 |