diff options
| -rw-r--r-- | clib/cStack.ml | 44 | ||||
| -rw-r--r-- | clib/cStack.mli | 58 | ||||
| -rw-r--r-- | clib/clib.mllib | 2 | ||||
| -rw-r--r-- | lib/util.ml | 4 | ||||
| -rw-r--r-- | lib/util.mli | 4 | ||||
| -rw-r--r-- | plugins/cc/ccalgo.mli | 1 |
6 files changed, 0 insertions, 113 deletions
diff --git a/clib/cStack.ml b/clib/cStack.ml deleted file mode 100644 index 0432e29fad..0000000000 --- a/clib/cStack.ml +++ /dev/null @@ -1,44 +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) *) -(************************************************************************) - -exception Empty = Stack.Empty - -type 'a t = { - mutable stack : 'a list; -} - -let create () = { stack = [] } - -let push x s = s.stack <- x :: s.stack - -let pop = function - | { stack = [] } -> raise Stack.Empty - | { stack = x::xs } as s -> s.stack <- xs; x - -let top = function - | { stack = [] } -> raise Stack.Empty - | { stack = x::_ } -> x - -let to_list { stack = s } = s - -let find f s = List.find f (to_list s) - -let find_map f s = CList.find_map f s.stack - -let fold_until f accu s = CList.fold_left_until f accu s.stack - -let is_empty { stack = s } = s = [] - -let iter f { stack = s } = List.iter f s - -let clear s = s.stack <- [] - -let length { stack = s } = List.length s - 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. *) - diff --git a/clib/clib.mllib b/clib/clib.mllib index 5a2c9a9ce9..be3b5971be 100644 --- a/clib/clib.mllib +++ b/clib/clib.mllib @@ -9,7 +9,6 @@ CSet CMap CList CString -CStack Int Range @@ -33,7 +32,6 @@ Unionfind Dyn Store Exninfo -Backtrace IStream Terminal Monad diff --git a/lib/util.ml b/lib/util.ml index e2447b005e..ae8119ced0 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -82,10 +82,6 @@ module Set = CSet module Map = CMap -(* Stacks *) - -module Stack = CStack - (* Matrices *) let matrix_transpose mat = diff --git a/lib/util.mli b/lib/util.mli index 1417d6dfcb..be0cc11763 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -76,10 +76,6 @@ module Set : module type of CSet module Map : module type of CMap -(** {6 Stacks.} *) - -module Stack : module type of CStack - (** {6 Streams. } *) val stream_nth : int -> 'a Stream.t -> 'a diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 3dc934b426..e1d7590ee2 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -8,7 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Util open Constr open Names |