functor (Ext : EXT) ->
  sig
    type t
    and ext = Ext.t
    val eq : Solution.SET.t -> Solution.SET.t -> bool
    val pp : Solution.SET.t Pretty.printer
    val empty : Solution.SET.t
    val is_empty : Solution.SET.t -> bool
    val is_dependent : Solution.SET.t -> Term.t -> bool
    val is_independent : Solution.SET.t -> Term.t -> bool
    val iter : (Fact.Equal.t -> unit) -> Solution.SET.t -> unit
    val fold : (Fact.Equal.t -> 'a -> 'a) -> Solution.SET.t -> 'a -> 'a
    val for_all : (Fact.Equal.t -> bool) -> Solution.SET.t -> bool
    val exists : (Fact.Equal.t -> bool) -> Solution.SET.t -> bool
    val to_list : Solution.SET.t -> Fact.Equal.t list
    val equality : Solution.SET.t -> Term.t -> Fact.Equal.t
    val apply : Solution.SET.t -> Jst.Eqtrans.t
    val find : Solution.SET.t -> Jst.Eqtrans.t
    val inv : Solution.SET.t -> Jst.Eqtrans.t
    val dep : Solution.SET.t -> Term.t -> Term.Var.Set.t
    val ext : Solution.SET.t -> Solution.SET.ext
    module Dep :
      sig
        type eqs = t
        val iter :
          Solution.DEP.eqs -> (Fact.Equal.t -> unit) -> Term.t -> unit
        val fold :
          Solution.DEP.eqs ->
          (Fact.Equal.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
        val for_all :
          Solution.DEP.eqs -> (Fact.Equal.t -> bool) -> Term.t -> bool
        val exists :
          Solution.DEP.eqs -> (Fact.Equal.t -> bool) -> Term.t -> bool
        val choose :
          Solution.DEP.eqs ->
          (Fact.Equal.t -> bool) -> Term.t -> Fact.Equal.t
      end
    val restrict : Solution.SET.t -> Term.t -> unit
    type config = Partition.t * Solution.SET.t
    val update : Solution.SET.config -> Fact.Equal.t -> unit
    val diff : Solution.SET.t -> Solution.SET.t -> Solution.SET.t
    val copy : Solution.SET.t -> Solution.SET.t
  end