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/typeops.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/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 3ec08fef48..294d99eeac 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -21,7 +21,7 @@ open Type_errors let conv_leq l2r = default_conv CUMUL ~l2r let conv_leq_vecti env v1 v2 = - array_fold_left2_i + Array.fold_left2_i (fun i c t1 t2 -> let c' = try default_conv CUMUL env t1 t2 @@ -476,7 +476,7 @@ and execute_recdef env (names,lar,vdef) i cu = univ_combinator cu2 ((lara.(i),(names,lara,vdefv)),cst) -and execute_array env = array_fold_map' (execute env) +and execute_array env = Array.fold_map' (execute env) (* Derived functions *) let infer env constr = |