diff options
| author | ppedrot | 2012-09-14 19:13:19 +0000 |
|---|---|---|
| committer | ppedrot | 2012-09-14 19:13:19 +0000 |
| commit | 8cc623262c625bda20e97c75f9ba083ae8e7760d (patch) | |
| tree | 3e7ef244636612606a574a21e4f8acaab828d517 /kernel/declarations.ml | |
| parent | 6eaff635db797d1f9225b22196832c1bb76c0d94 (diff) | |
As r15801: putting everything from Util.array_* to CArray.*.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15804 85f007b7-540e-0410-9357-904b9bb8a0f7
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 } |