sig
  val pp_index : bool Pervasives.ref
  module type DEP =
    sig
      type eqs
      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
  module type SET =
    sig
      type t
      and ext
      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
  module type EXT =
    sig
      type t
      val pp : Solution.EXT.t Pretty.printer
      val empty : Solution.EXT.t
      val update : Solution.EXT.t -> Fact.Equal.t -> Solution.EXT.t
      val restrict : Solution.EXT.t -> Fact.Equal.t -> Solution.EXT.t
    end
  module Make :
    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
  module type SET0 =
    sig
      type t
      and ext = unit
      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
  module Set : SET0
  module Proj : functor (S : SET) -> SET0
end