aboutsummaryrefslogtreecommitdiff
path: root/clib/cStack.mli
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2020-03-10 03:41:20 -0400
committerEmilio Jesus Gallego Arias2020-03-10 03:41:20 -0400
commit4e5ed2d6ba574ee6449e511dc27e8da32331dd07 (patch)
tree1c01577abed111554976fe7127f90b4fc994c8fe /clib/cStack.mli
parentbab342d98d413a2b7a20da98c8dbec7616f54bce (diff)
[clib] Remove module CStack
This is only used in `Ccalgo` and it does not provide any advantage these days over the upstream OCaml implementation.
Diffstat (limited to 'clib/cStack.mli')
-rw-r--r--clib/cStack.mli58
1 files changed, 0 insertions, 58 deletions
diff --git a/clib/cStack.mli b/clib/cStack.mli
deleted file mode 100644
index de802160e7..0000000000
--- a/clib/cStack.mli
+++ /dev/null
@@ -1,58 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(** Extended interface for OCaml stacks. *)
-
-type 'a t
-
-exception Empty
-(** Alias for Stack.Empty. *)
-
-val create : unit -> '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. *)
-
-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. *)
-