(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id$ *)

module type Comparable =
  sig
    type t
    val is_eq : t -> t -> bool
  end

module C : Comparable 

module FotermIndexable : Discrimination_tree.Indexable
with type constant_name = C.t and
     type input = C.t Terms.foterm 

module ClauseSet : Set.S with type elt = Terms.direction * C.t Terms.unit_clause

module DiscriminationTree : Discrimination_tree.DiscriminationTree 
with type constant_name = C.t
and type input = C.t Terms.foterm
and type data = ClauseSet.elt and type dataset = ClauseSet.t