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

Reviewed-by: ppedrot

1 files changed, 0 insertions, 97 deletions

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))
-*)