diff options
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 34 |
1 files changed, 15 insertions, 19 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 3e89112ae3..8770afe131 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -266,26 +266,22 @@ and constants_of_modtype env mp modtype = (* returns a resolver for kn that maps mbid to mp *) let resolver_of_environment mbid modtype mp env = let constants = constants_of_modtype env (MPbound mbid) modtype in - let resolve = - List.map - (fun (con,expecteddef) -> - let con' = replace_mp_in_con (MPbound mbid) mp con in - let constr = - try - if expecteddef.Declarations.const_inline then - let constant = lookup_constant con' env in - if constant.Declarations.const_opaque then - None - else - option_map Declarations.force - constant.Declarations.const_body - else - None - with Not_found -> error_no_such_label (con_label con') - in - con,constr - ) constants + let rec make_resolve = function + | [] -> [] + | (con,expecteddef)::r -> + let con' = replace_mp_in_con (MPbound mbid) mp con in + try + if expecteddef.Declarations.const_inline then + let constant = lookup_constant con' env in + if (not constant.Declarations.const_opaque) then + let constr = option_map Declarations.force + constant.Declarations.const_body in + (con,constr)::(make_resolve r) + else make_resolve r + else make_resolve r + with Not_found -> error_no_such_label (con_label con') in + let resolve = make_resolve constants in Mod_subst.make_resolver resolve let strengthen_const env mp l cb = |