diff options
Diffstat (limited to 'kernel/declarations.ml')
| -rw-r--r-- | kernel/declarations.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/kernel/declarations.ml b/kernel/declarations.ml index a2ce4f2705..b8edcae726 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -325,10 +325,10 @@ let subst_mind_packet sub mbp = { mind_consnames = mbp.mind_consnames; mind_consnrealdecls = mbp.mind_consnrealdecls; mind_typename = mbp.mind_typename; - mind_nf_lc = array_smartmap (subst_mps sub) mbp.mind_nf_lc; + mind_nf_lc = Array.smartmap (subst_mps sub) mbp.mind_nf_lc; mind_arity_ctxt = subst_rel_context sub mbp.mind_arity_ctxt; mind_arity = subst_indarity sub mbp.mind_arity; - mind_user_lc = array_smartmap (subst_mps sub) mbp.mind_user_lc; + mind_user_lc = Array.smartmap (subst_mps sub) mbp.mind_user_lc; mind_nrealargs = mbp.mind_nrealargs; mind_nrealargs_ctxt = mbp.mind_nrealargs_ctxt; mind_kelim = mbp.mind_kelim; @@ -346,7 +346,7 @@ let subst_mind sub mib = mind_nparams_rec = mib.mind_nparams_rec; mind_params_ctxt = map_rel_context (subst_mps sub) mib.mind_params_ctxt; - mind_packets = array_smartmap (subst_mind_packet sub) mib.mind_packets ; + mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ; mind_constraints = mib.mind_constraints } let hcons_indarity = function @@ -360,13 +360,13 @@ let hcons_mind_packet oib = mind_typename = hcons_ident oib.mind_typename; mind_arity_ctxt = hcons_rel_context oib.mind_arity_ctxt; mind_arity = hcons_indarity oib.mind_arity; - mind_consnames = array_smartmap hcons_ident oib.mind_consnames; - mind_user_lc = array_smartmap hcons_types oib.mind_user_lc; - mind_nf_lc = array_smartmap hcons_types oib.mind_nf_lc } + mind_consnames = Array.smartmap hcons_ident oib.mind_consnames; + mind_user_lc = Array.smartmap hcons_types oib.mind_user_lc; + mind_nf_lc = Array.smartmap hcons_types oib.mind_nf_lc } let hcons_mind mib = { mib with - mind_packets = array_smartmap hcons_mind_packet mib.mind_packets; + mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; mind_constraints = hcons_constraints mib.mind_constraints } |