functor (E : LogtkIndex.EQUATION->
  sig
    type t
    module E :
      sig
        type t = E.t
        type rhs = E.rhs
        val compare : t -> t -> int
        val extract : t -> LogtkIndex.term * rhs * bool
        val priority : t -> int
      end
    type rhs = E.rhs
    val empty : unit -> t
    val is_empty : t -> bool
    val add : t -> E.t -> t
    val add_seq : t -> E.t Sequence.t -> t
    val remove : t -> E.t -> t
    val remove_seq : t -> E.t Sequence.t -> t
    val size : t -> int
    val iter : t -> (LogtkIndex.term -> E.t -> unit) -> unit
    val retrieve :
      ?allow_open:bool ->
      ?subst:LogtkIndex.subst ->
      sign:bool ->
      t ->
      LogtkIndex.scope ->
      LogtkIndex.term ->
      LogtkIndex.scope ->
      '->
      ('-> LogtkIndex.term -> rhs -> E.t -> LogtkIndex.subst -> 'a) -> 'a
    val to_dot : Buffer.t -> t -> unit
  end