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/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 'checker/typeops.ml')
| -rw-r--r-- | checker/typeops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/checker/typeops.ml b/checker/typeops.ml index 03d2bedcf..91f58a04a 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -20,7 +20,7 @@ open Environ let inductive_of_constructor = fst let conv_leq_vecti env v1 v2 = - array_fold_left2_i + Array.fold_left2_i (fun i _ t1 t2 -> (try conv_leq env t1 t2 with NotConvertible -> raise (NotConvertibleVect i)); ()) @@ -244,7 +244,7 @@ let type_fixpoint env lna lar lbody vdefj = try conv_leq_vecti env vdefj (Array.map (fun ty -> lift lt ty) lar) with NotConvertibleVect i -> - let vdefj = array_map2 (fun b ty -> b,ty) lbody vdefj in + let vdefj = Array.map2 (fun b ty -> b,ty) lbody vdefj in error_ill_typed_rec_body env i lna vdefj lar (************************************************************************) @@ -293,7 +293,7 @@ let rec execute env cstr = (* No sort-polymorphism *) execute env f in - let jl = array_map2 (fun c ty -> c,ty) args jl in + let jl = Array.map2 (fun c ty -> c,ty) args jl in judge_of_apply env (f,j) jl | Lambda (name,c1,c2) -> @@ -362,7 +362,7 @@ and execute_type env constr = and execute_recdef env (names,lar,vdef) i = let larj = execute_array env lar in - let larj = array_map2 (fun c ty -> c,ty) lar larj in + let larj = Array.map2 (fun c ty -> c,ty) lar larj in let lara = Array.map (assumption_of_judgment env) larj in let env1 = push_rec_types (names,lara,vdef) env in let vdefj = execute_array env1 vdef in |