Merge PR #11790: [lib] [ccalgo] Remove unused code / cleanup

Reviewed-by: ppedrot

6 files changed, 0 insertions, 209 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..b0b74f4558 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
 
@@ -156,102 +155,6 @@ val subterms : forest -> int -> int * int
 val join_path : forest -> int -> int ->
   ((int * int) * equality) list * ((int * int) * equality) list
 
-val make_fun_table : state -> Int.Set.t PafMap.t
-
-val do_match :  state ->
-    (quant_eq * int array) list ref -> matching_problem Stack.t -> unit
-
-val init_pb_stack : state -> matching_problem Stack.t
-
-val paf_of_patt : int Termhash.t -> ccpattern -> pa_fun
-
-val find_instances : state -> (quant_eq * int array) list
-
 val execute : bool -> state -> explanation option
 
 val pr_idx_term : Environ.env -> Evd.evar_map -> forest -> int -> Pp.t
-
-val empty_forest: unit -> forest
-
-
-
-
-
-
-
-
-
-
-(*type pa_constructor
-
-
-module PacMap:CSig.MapS with type key=pa_constructor
-
-type term =
-    Symb of Term.constr
-  | Eps
-  | Appli of term * term
-  | Constructor of Names.constructor*int*int
-
-type rule =
-    Congruence
-  | Axiom of Names.Id.t
-  | Injection of int*int*int*int
-
-type equality =
-    {lhs : int;
-     rhs : int;
-     rule : rule}
-
-module ST :
-sig
-  type t
-  val empty : unit -> t
-  val enter : int -> int * int -> t -> unit
-  val query : int * int -> t -> int
-  val delete : int -> t -> unit
-  val delete_list : int list -> t -> unit
-end
-
-module UF :
-sig
-  type t
-  exception Discriminable of int * int * int * int * t
-  val empty : unit -> t
-  val find : t -> int -> int
-  val size : t -> int -> int
-  val get_constructor : t -> int -> Names.constructor
-  val pac_arity : t -> int -> int * int -> int
-  val mem_node_pac : t -> int -> int * int -> int
-  val add_pacs : t -> int -> pa_constructor PacMap.t ->
-    int list * equality list
-  val term : t -> int -> term
-  val subterms : t -> int -> int * int
-  val add : t -> term -> int
-  val union : t -> int -> int -> equality -> int list * equality list
-  val join_path : t -> int -> int ->
-    ((int*int)*equality) list*
-    ((int*int)*equality) list
-end
-
-
-val combine_rec : UF.t -> int list -> equality list
-val process_rec : UF.t -> equality list -> int list
-
-val cc : UF.t -> unit
-
-val make_uf :
-  (Names.Id.t * (term * term)) list -> UF.t
-
-val add_one_diseq : UF.t -> (term * term) -> int * int
-
-val add_disaxioms :
-  UF.t -> (Names.Id.t * (term * term)) list ->
-  (Names.Id.t * (int * int)) list
-
-val check_equal : UF.t -> int * int -> bool
-
-val find_contradiction : UF.t ->
-  (Names.Id.t * (int * int)) list ->
-  (Names.Id.t * (int * int))
-*)