diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 19:13:19 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-09-14 19:13:19 +0000 |
| commit | 8cc623262c625bda20e97c75f9ba083ae8e7760d (patch) | |
| tree | 3e7ef244636612606a574a21e4f8acaab828d517 /checker/subtyping.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 'checker/subtyping.ml')
| -rw-r--r-- | checker/subtyping.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 55ed06665..7d2ced7fd 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -42,7 +42,7 @@ let add_mib_nameobjects mp l mib map = let add_mip_nameobjects j oib map = let ip = (ind,j) in let map = - array_fold_right_i + Array.fold_right_i (fun i id map -> Labmap.add (label_of_id id) (IndConstr((ip,i+1), mib)) map) oib.mind_consnames @@ -50,7 +50,7 @@ let add_mib_nameobjects mp l mib map = in Labmap.add (label_of_id oib.mind_typename) (IndType (ip, mib)) map in - array_fold_right_i add_mip_nameobjects mib.mind_packets map + Array.fold_right_i add_mip_nameobjects mib.mind_packets map (* creates (namedobject/namedmodule) map for the whole signature *) @@ -149,7 +149,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= (type_of_inductive env (mib1,p1)) (type_of_inductive env (mib2,p2)) in let check_cons_types i p1 p2 = - array_iter2 (check_conv conv env) + Array.iter2 (check_conv conv env) (arities_of_specif kn (mib1,p1)) (arities_of_specif kn (mib2,p2)) in @@ -194,9 +194,9 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= check (fun mib -> names_prod_letin mib.mind_packets.(0).mind_user_lc.(0)); end; (* we first check simple things *) - array_iter2 check_packet mib1.mind_packets mib2.mind_packets; + Array.iter2 check_packet mib1.mind_packets mib2.mind_packets; (* and constructor types in the end *) - let _ = array_map2_i check_cons_types mib1.mind_packets mib2.mind_packets + let _ = Array.map2_i check_cons_types mib1.mind_packets mib2.mind_packets in () let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = |