diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declaremods.ml | 20 | ||||
| -rw-r--r-- | library/impargs.ml | 2 | ||||
| -rw-r--r-- | library/libnames.ml | 14 | ||||
| -rw-r--r-- | library/libnames.mli | 2 |
4 files changed, 21 insertions, 17 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index e1a27314f..ddcfd1bcd 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -698,21 +698,25 @@ let declare_modtype interp_modtype id args mty = ignore (add_leaf id (in_modtype (Some entry, substobjs))) - -let rec get_module_substobjs = function +let rec get_module_substobjs env = function | MEident mp -> MPmap.find mp !modtab_substobjs | MEfunctor (mbid,mty,mexpr) -> - let (subst, mbids, msid, objs) = - get_module_substobjs mexpr - in + let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (subst, mbid::mbids, msid, objs) | MEstruct (msid,_) -> (empty_subst, [], msid, []) | MEapply (mexpr, MEident mp) -> - let (subst, mbids, msid, objs) = get_module_substobjs mexpr in + let feb,ftb = Mod_typing.translate_mexpr env mexpr in + let ftb = Modops.scrape_modtype env ftb in + let farg_id, farg_b, fbody_b = Modops.destr_functor ftb in + let (subst, mbids, msid, objs) = get_module_substobjs env mexpr in (match mbids with | mbid::mbids -> - (add_mbid mbid mp subst, mbids, msid, objs) + let resolve = + 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) | [] -> match mexpr with | MEident _ | MEstruct _ -> error "Application of a non-functor" | _ -> error "Application of a functor with too few arguments") @@ -758,7 +762,7 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o = let substobjs = match entry with | {mod_entry_type = Some mte} -> get_modtype_substobjs mte - | {mod_entry_expr = Some mexpr} -> get_module_substobjs mexpr + | {mod_entry_expr = Some mexpr} -> get_module_substobjs env mexpr | _ -> anomaly "declare_module: No type, no body ..." in Summary.unfreeze_summaries fs; diff --git a/library/impargs.ml b/library/impargs.ml index d77543367..8daf939ef 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -358,7 +358,7 @@ let cache_implicits_decl (r,imps) = let cache_implicits (_,l) = List.iter cache_implicits_decl l let subst_implicits_decl subst (r,imps as o) = - let r' = subst_global subst r in if r==r' then o else (r',imps) + let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) let subst_implicits (_,subst,l) = list_smartmap (subst_implicits_decl subst) l diff --git a/library/libnames.ml b/library/libnames.ml index fd5bb2196..f21b98698 100644 --- a/library/libnames.ml +++ b/library/libnames.ml @@ -22,16 +22,16 @@ type global_reference = | ConstructRef of constructor let subst_global subst ref = match ref with - | VarRef _ -> ref + | VarRef var -> ref, mkVar var | ConstRef kn -> - let kn' = subst_con subst kn in if kn==kn' then ref else - ConstRef kn' + let kn',t = subst_con subst kn in + if kn==kn' then ref, mkConst kn else ConstRef kn', t | IndRef (kn,i) -> - let kn' = subst_kn subst kn in if kn==kn' then ref else - IndRef(kn',i) + let kn' = subst_kn subst kn in if kn==kn' then ref, mkInd (kn,i) else + IndRef(kn',i), mkInd (kn',i) | ConstructRef ((kn,i),j) -> - let kn' = subst_kn subst kn in if kn==kn' then ref else - ConstructRef ((kn',i),j) + let kn' = subst_kn subst kn in if kn==kn' then ref, mkConstruct ((kn,i),j) + else ConstructRef ((kn',i),j), mkConstruct ((kn',i),j) let reference_of_constr c = match kind_of_term c with | Const sp -> ConstRef sp diff --git a/library/libnames.mli b/library/libnames.mli index b2c32f89b..379ce64b4 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -23,7 +23,7 @@ type global_reference = | IndRef of inductive | ConstructRef of constructor -val subst_global : substitution -> global_reference -> global_reference +val subst_global : substitution -> global_reference -> global_reference * constr (* Turn a global reference into a construction *) val constr_of_reference : global_reference -> constr |