1 files changed, 39 insertions, 45 deletions
diff --git a/contrib/cc/ccalgo.mli b/contrib/cc/ccalgo.mli
index 6f55d8541..582df715f 100644
--- a/contrib/cc/ccalgo.mli
+++ b/contrib/cc/ccalgo.mli
@@ -10,58 +10,52 @@
 
 val init_size : int
 
-type term = Symb of Term.constr | Appli of term * term
+type term = 
+    Symb of Term.constr 
+  | Appli of term * term 
 
-module UF :
-  sig
-    type tag = Congr | Ax of Names.identifier
-    and cl =
-        Rep of int * int list
-      | Eqto of int * (int * int * tag)
-    and vertex = Leaf | Node of (int * int)
-    and t = int ref * (int, cl * vertex * term) Hashtbl.t
-    val empty : unit -> t
-    val add_lst : int -> int -> t -> unit
-    val find : t -> int -> int
-    val list : t -> int -> int list
-    val size : t -> int -> int
-    val signature : t -> int -> int * int
-    val nodes : t -> int list
-    val add :
-      term ->
-      int ref * (int, cl * vertex * term) Hashtbl.t ->
-      (term, int) Hashtbl.t -> int
-    val union :
-      t -> int -> int -> int * int * tag -> unit
-  end
-
-module ST :
-  sig
-    type t =
-      (int * int, int) Hashtbl.t *
-      (int, int * int) Hashtbl.t
-    val empty :
-      unit -> ('a, 'b) Hashtbl.t * ('c, 'd) Hashtbl.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
+type rule = 
+    Congruence 
+  | Axiom of Names.identifier      
 
-val combine_rec :
-  UF.t -> ST.t -> int list -> (int * int) list
+type valid =
+    {lhs : int; 
+     rhs : int; 
+     rule : rule}
 
-val process_rec :
-  UF.t -> ST.t -> (int * int) list -> int list
+module UF :
+sig
+  type t 
+  val empty : unit -> t
+  val add_lst : int -> int -> t -> unit
+  val find : t -> int -> int
+  val list : t -> int -> int list
+  val size : t -> int -> int
+  val term : t -> int -> term    
+  val subterms : t -> int -> int * int
+  val signature : t -> int -> int * int
+  val nodes : t -> int list
+  val add : term -> t -> int
+  val union : t -> int -> int -> valid -> unit
+  val join_path : t -> int -> int -> 
+    ((int*int)*valid) list*
+    ((int*int)*valid) list
+end
+
+  
+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
 
-val cc_rec : UF.t -> ST.t -> int list -> unit
 
 val cc : UF.t -> unit
 
 val make_uf :
-  (term, int) Hashtbl.t ->
   (Names.identifier * (term * term)) list -> UF.t
 
-val decide_prb :
-  (Names.identifier * (term * term)) list * (term * term) ->
-  bool