summaryrefslogtreecommitdiff
path: root/library/declaremods.ml
diff options
context:
space:
mode:
Diffstat (limited to 'library/declaremods.ml')
-rw-r--r--library/declaremods.ml90
1 files changed, 45 insertions, 45 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 3026143b..93021384 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 11898 2009-02-10 10:52:45Z soubiran $ i*)
+(*i $Id: declaremods.ml 12204 2009-06-22 16:06:49Z soubiran $ i*)
open Pp
open Util
open Names
@@ -642,29 +642,30 @@ let rec get_modtype_substobjs env = function
(subst_key (map_msid msid mp) sub_alias)
(map_msid msid mp)
| _ -> sub_alias in
- let sub3=
+ let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
+ let mbid,mbids= (match mbids with
+ | mbid::mbids -> mbid,mbids
+ | [] -> match mexpr with
+ | MSEident _ -> error "Application of a non-functor"
+ | _ -> error "Application of a functor with too few arguments") in
+ let resolve =
+ Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
+ let sub3=
if sub1 = empty_subst then
- update_subst sub_alias (map_mbid farg_id mp None)
+ update_subst sub_alias (map_mbid farg_id mp (Some resolve))
else
- let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
+ let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
let sub_alias' = update_subst sub_alias sub1' in
join sub1' sub_alias'
in
- let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in
- let (subst, mbids, msid, objs) = get_modtype_substobjs env mexpr in
- (match mbids with
- | mbid::mbids ->
- let resolve =
- Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
- (* application outside the kernel, only for substitutive
- objects (that are all non-logical objects) *)
- ((join
- (join subst sub3)
- (map_mbid mbid mp (Some resolve)))
- , mbids, msid, objs)
- | [] -> match mexpr with
- | MSEident _ -> error "Application of a non-functor"
- | _ -> error "Application of a functor with too few arguments")
+ let sub3 = join sub3
+ (update_subst sub_alias (map_mbid farg_id mp (Some resolve))) in
+ (* application outside the kernel, only for substitutive
+ objects (that are all non-logical objects) *)
+ ((join
+ (join subst sub3)
+ (map_mbid mbid mp (Some resolve)))
+ , mbids, msid, objs)
| MSEapply (_,mexpr) ->
Modops.error_application_to_not_path mexpr
@@ -948,30 +949,32 @@ let rec get_module_substobjs env = function
(subst_key (map_msid msid mp) sub_alias)
(map_msid msid mp)
| _ -> sub_alias in
-
+ let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
+ let mbid,mbids =
+ (match mbids with
+ | mbid::mbids ->mbid,mbids
+
+ | [] -> match mexpr with
+ | MSEident _ -> error "Application of a non-functor"
+ | _ -> error "Application of a functor with too few arguments") in
+ let resolve =
+ Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
let sub3=
if sub1 = empty_subst then
- update_subst sub_alias (map_mbid farg_id mp None)
+ update_subst sub_alias (map_mbid farg_id mp (Some resolve))
else
- let sub1' = join_alias sub1 (map_mbid farg_id mp None) in
+ let sub1' = join_alias sub1 (map_mbid farg_id mp (Some resolve)) in
let sub_alias' = update_subst sub_alias sub1' in
- join sub1' sub_alias'
+ join sub1' sub_alias'
in
- let sub3 = join sub3 (update_subst sub_alias (map_mbid farg_id mp None)) in
- let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in
- (match mbids with
- | mbid::mbids ->
- let resolve =
- Modops.resolver_of_environment farg_id farg_b mp sub_alias env in
- (* application outside the kernel, only for substitutive
- objects (that are all non-logical objects) *)
- ((join
- (join subst sub3)
- (map_mbid mbid mp (Some resolve)))
- , mbids, msid, objs)
- | [] -> match mexpr with
- | MSEident _ -> error "Application of a non-functor"
- | _ -> error "Application of a functor with too few arguments")
+ let sub3 = join sub3 (update_subst sub_alias
+ (map_mbid farg_id mp (Some resolve))) in
+ (* application outside the kernel, only for substitutive
+ objects (that are all non-logical objects) *)
+ ((join
+ (join subst sub3)
+ (map_mbid mbid mp (Some resolve)))
+ , mbids, msid, objs)
| MSEapply (_,mexpr) ->
Modops.error_application_to_not_path mexpr
| MSEwith (mty, With_Definition _) -> get_module_substobjs env mty
@@ -1061,12 +1064,9 @@ let rec update_include (sub,mbids,msid,objs) =
| (id,obj)::tail ->
if object_tag obj = "INCLUDE" then
let ((me,is_mod),substobjs,substituted) = out_include obj in
- if not (is_mod) then
- let substobjs' = update_include substobjs in
- (id, in_include ((me,true),substobjs',substituted))::
- (replace_include tail)
- else
- (id,obj)::(replace_include tail)
+ let substobjs' = update_include substobjs in
+ (id, in_include ((me,true),substobjs',substituted))::
+ (replace_include tail)
else
(id,obj)::(replace_include tail)
in
@@ -1142,7 +1142,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
| _ ->
let dir,mp = dir_of_sp (Lib.make_path id), mp_of_kn (Lib.make_kn id) in
let (sub,mbids,msid,objs) = substobjs in
- let sub' = subst_key (map_msid msid mp) sub in
+ let sub' = join_alias (subst_key (map_msid msid mp) sub) (map_msid msid mp) in
let substobjs = (join sub sub',mbids,msid,objs) in
let substituted = subst_substobjs dir mp substobjs in
ignore (add_leaf