(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* 'a t (** Create an empty stack. *) val push : 'a -> 'a t -> unit (** Add an element to a stack. *) val find : ('a -> bool) -> 'a t -> 'a (** Find the first element satisfying the predicate. @raise Not_found it there is none. *) val is_empty : 'a t -> bool (** Whether a stack is empty. *) val iter : ('a -> unit) -> 'a t -> unit (** Iterate a function over elements, from the last added one. *) val clear : 'a t -> unit (** Empty a stack. *) val length : 'a t -> int (** Length of a stack. *) val pop : 'a t -> 'a (** Remove and returns the first element of the stack. @raise Empty if empty. *) val top : 'a t -> 'a (** Remove the first element of the stack without modifying it. @raise Empty if empty. *) val to_list : 'a t -> 'a list (** Convert to a list. *) 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