[clib] Remove module CStack

This is only used in `Ccalgo` and it does not provide any advantage
these days over the upstream OCaml implementation.

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