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 /pretyping/cases.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 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 196f5a0e7e..0ece3496e1 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1016,7 +1016,7 @@ let rec ungeneralize n ng body = let sign2,p = decompose_prod_n_assum ng p in let p = prod_applist p [mkRel (n+List.length sign+ng)] in it_mkLambda_or_LetIn (it_mkProd_or_LetIn p sign2) sign in - mkCase (ci,p,c,array_map2 (fun q c -> + mkCase (ci,p,c,Array.map2 (fun q c -> let sign,b = decompose_lam_n_assum q c in it_mkLambda_or_LetIn (ungeneralize (n+q) ng b) sign) ci.ci_cstr_ndecls brs) @@ -1046,7 +1046,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs = let pred = lift_predicate (-1) pred tomatch in let tomatch = relocate_index_tomatch 1 (n+1) tomatch in let tomatch = lift_tomatch_stack (-1) tomatch in - let brs = array_map2 (ungeneralize_branch n k) brs cs in + let brs = Array.map2 (ungeneralize_branch n k) brs cs in aux k brs tomatch pred tocheck deps | _ -> assert false in aux 0 brs tomatch pred tocheck deps @@ -1255,7 +1255,7 @@ and match_current pb tomatch = let pb,deps = generalize_problem (names,dep) pb deps in (* We compile branches *) - let brvals = array_map2 (compile_branch current realargs (names,dep) deps pb arsign) eqns cstrs in + let brvals = Array.map2 (compile_branch current realargs (names,dep) deps pb arsign) eqns cstrs in (* We build the (elementary) case analysis *) let depstocheck = current::binding_vars_of_inductive typ in let brvals,tomatch,pred,inst = |