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 /library | |
| 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 'library')
| -rw-r--r-- | library/impargs.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index baf2e30ec6..cc4a4e45ef 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -168,8 +168,8 @@ let push_lift d (e,n) = (push_rel d e,n+1) let is_reversible_pattern bound depth f l = isRel f & let n = destRel f in (n < bound+depth) & (n >= depth) & - array_for_all (fun c -> isRel c & destRel c < depth) l & - array_distinct l + Array.for_all (fun c -> isRel c & destRel c < depth) l & + Array.distinct l (* Precondition: rels in env are for inductive types only *) let add_free_rels_until strict strongly_strict revpat bound env m pos acc = @@ -413,7 +413,7 @@ let compute_mib_implicits flags manual kn = let compute_all_mib_implicits flags manual kn = let imps = compute_mib_implicits flags manual kn in List.flatten - (array_map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) + (Array.map_to_list (fun (ind,cstrs) -> ind::Array.to_list cstrs) imps) (*s Variables. *) @@ -606,7 +606,7 @@ let declare_constant_implicits con = let declare_mib_implicits kn = let flags = !implicit_args in - let imps = array_map_to_list + let imps = Array.map_to_list (fun (ind,cstrs) -> ind::(Array.to_list cstrs)) (compute_mib_implicits flags [] kn) in add_anonymous_leaf |