From 4e13159efc009d8f534a3502124a1b8148407b24 Mon Sep 17 00:00:00 2001
From: gareuselesinge
Date: Thu, 10 Oct 2013 11:22:49 +0000
Subject: 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
---
 lib/cStack.mli | 10 +++-------
 1 file changed, 3 insertions(+), 7 deletions(-)

(limited to 'lib/cStack.mli')

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. *)
 
-- 
cgit v1.2.3