diff options
| author | gareuselesinge | 2013-10-10 11:22:49 +0000 |
|---|---|---|
| committer | gareuselesinge | 2013-10-10 11:22:49 +0000 |
| commit | 4e13159efc009d8f534a3502124a1b8148407b24 (patch) | |
| tree | aca63bbd6c68471da9546bce159cf75cfc82b104 /lib/cStack.mli | |
| parent | a8e4bc45bad59f24cddc6c10be83be2d14c1bc57 (diff) | |
Clib: fold_left_until added to CList
CStack just calls it to implement fold_until.
CSig.seek renamed CSig.until, since there is no seek function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16867 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/cStack.mli')
| -rw-r--r-- | lib/cStack.mli | 10 |
1 files changed, 3 insertions, 7 deletions
diff --git a/lib/cStack.mli b/lib/cStack.mli index 12bec14572..8dde1d1a1a 100644 --- a/lib/cStack.mli +++ b/lib/cStack.mli @@ -50,11 +50,7 @@ val find_map : ('a -> 'b option) -> 'a t -> 'b (** Find the first element that returns [Some _]. @raise Not_found it there is none. *) -type ('b, 'c) seek = ('b, 'c) CSig.seek = Stop of 'b | Next of 'c - -(** [seek f acc s] acts like [List.fold_left f acc s] while [f] returns - [Next acc']; it stops returning [b] as soon as [f] returns [Stop b]. - The stack is traversed from the top and is not altered. - @raise Not_found it there is none. *) -val fold_until : ('c -> 'a -> ('b, 'c) seek) -> 'c -> 'a t -> 'b +val fold_until : ('c -> 'a -> 'c CSig.until) -> 'c -> 'a t -> 'c +(** Like CList.fold_left_until. + The stack is traversed from the top and is not altered. *) |