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 /plugins/extraction/mlutil.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 'plugins/extraction/mlutil.ml')
| -rw-r--r-- | plugins/extraction/mlutil.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 3716695b8..01b98b131 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -524,7 +524,7 @@ let has_deep_pattern br = | Pcons (_,l) | Ptuple l -> not (List.for_all is_basic_pattern l) | Pusual _ | Prel _ | Pwild -> false in - array_exists (function (_,pat,_) -> deep pat) br + Array.exists (function (_,pat,_) -> deep pat) br let is_regular_match br = if Array.length br = 0 then false (* empty match becomes MLexn *) @@ -543,7 +543,7 @@ let is_regular_match br = | ConstructRef (ind,_) -> ind | _ -> raise Impossible in - array_for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br + Array.for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br with Impossible -> false (*S Operations concerning lambdas. *) @@ -770,7 +770,7 @@ let is_opt_pat (_,p,_) = match p with | _ -> false let factor_branches o typ br = - if array_exists is_opt_pat br then None (* already optimized *) + if Array.exists is_opt_pat br then None (* already optimized *) else begin census_clean (); for i = 0 to Array.length br - 1 do |