diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index ab187dba..98a99731 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -129,10 +129,10 @@ let destr_nofunctor = function |NoFunctor a -> a |MoreFunctor _ -> error_is_a_functor () -let rec functor_smartmap fty f0 funct = match funct with +let rec functor_smart_map fty f0 funct = match funct with |MoreFunctor (mbid,ty,e) -> let ty' = fty ty in - let e' = functor_smartmap fty f0 e in + let e' = functor_smart_map fty f0 e in if ty==ty' && e==e' then funct else MoreFunctor (mbid,ty',e') |NoFunctor a -> let a' = f0 a in if a==a' then funct else NoFunctor a' @@ -196,7 +196,7 @@ let rec subst_structure sub do_delta sign = let mtb' = subst_modtype sub do_delta mtb in if mtb==mtb' then orig else (l,SFBmodtype mtb') in - List.smartmap subst_body sign + List.Smart.map subst_body sign and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = fun is_mod sub subst_impl do_delta mb -> @@ -209,7 +209,7 @@ and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> in let ty' = subst_signature sub do_delta ty in let me' = subst_impl sub me in - let aty' = Option.smartmap (subst_expression sub id_delta) aty in + let aty' = Option.Smart.map (subst_expression sub id_delta) aty in let delta' = do_delta mb.mod_delta sub in if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta then mb @@ -244,12 +244,12 @@ and subst_expr sub do_delta seb = match seb with if meb==meb' && wdb==wdb' then seb else MEwith(meb',wdb') and subst_expression sub do_delta = - functor_smartmap + functor_smart_map (subst_modtype sub do_delta) (subst_expr sub do_delta) and subst_signature sub do_delta = - functor_smartmap + functor_smart_map (subst_modtype sub do_delta) (subst_structure sub do_delta) @@ -265,7 +265,7 @@ let subst_structure subst = subst_structure subst do_delta_codom (* spiwack: here comes the function which takes care of importing the retroknowledge declared in the library *) (* lclrk : retroknowledge_action list, rkaction : retroknowledge action *) -let add_retroknowledge mp = +let add_retroknowledge = let perform rkaction env = match rkaction with | Retroknowledge.RKRegister (f, e) when (isConst e || isInd e) -> Environ.register env f e @@ -309,7 +309,7 @@ and add_module mb linkinfo env = let env = Environ.shallow_add_module mb env in match mb.mod_type with |NoFunctor struc -> - add_retroknowledge mp mb.mod_retroknowledge + add_retroknowledge mb.mod_retroknowledge (add_structure mp struc mb.mod_delta linkinfo env) |MoreFunctor _ -> env @@ -402,7 +402,8 @@ let inline_delta_resolver env inl mp mbid mtb delta = | Undef _ | OpaqueDef _ -> l | Def body -> let constr = Mod_subst.force_constr body in - add_inline_delta_resolver kn (lev, Some constr) l + let ctx = Declareops.constant_polymorphic_context constant in + add_inline_delta_resolver kn (lev, Some (ctx, constr)) l with Not_found -> error_no_such_label_sub (Constant.label con) (ModPath.to_string (Constant.modpath con)) @@ -594,13 +595,13 @@ and clean_field l field = match field with if mb==mb' then field else (lab,SFBmodule mb') |_ -> field -and clean_structure l = List.smartmap (clean_field l) +and clean_structure l = List.Smart.map (clean_field l) and clean_signature l = - functor_smartmap (clean_module_type l) (clean_structure l) + functor_smart_map (clean_module_type l) (clean_structure l) and clean_expression l = - functor_smartmap (clean_module_type l) (fun me -> me) + functor_smart_map (clean_module_type l) (fun me -> me) let rec collect_mbid l sign = match sign with |MoreFunctor (mbid,ty,m) -> |