sig
  module S :
    sig
      type t
      and ext = Term.Var.Set.t
      val eq : t -> t -> bool
      val pp : t Pretty.printer
      val empty : t
      val is_empty : t -> bool
      val is_dependent : t -> Term.t -> bool
      val is_independent : t -> Term.t -> bool
      val iter : (Fact.Equal.t -> unit) -> t -> unit
      val fold : (Fact.Equal.t -> 'a -> 'a) -> t -> 'a -> 'a
      val for_all : (Fact.Equal.t -> bool) -> t -> bool
      val exists : (Fact.Equal.t -> bool) -> t -> bool
      val to_list : t -> Fact.Equal.t list
      val equality : t -> Term.t -> Fact.Equal.t
      val apply : t -> Jst.Eqtrans.t
      val find : t -> Jst.Eqtrans.t
      val inv : t -> Jst.Eqtrans.t
      val dep : t -> Term.t -> Term.Var.Set.t
      val ext : t -> ext
      module Dep :
        sig
          type eqs = t
          val iter : eqs -> (Fact.Equal.t -> unit) -> Term.t -> unit
          val fold : eqs -> (Fact.Equal.t -> 'a -> 'a) -> Term.t -> 'a -> 'a
          val for_all : eqs -> (Fact.Equal.t -> bool) -> Term.t -> bool
          val exists : eqs -> (Fact.Equal.t -> bool) -> Term.t -> bool
          val choose :
            eqs -> (Fact.Equal.t -> bool) -> Term.t -> Fact.Equal.t
        end
      val restrict : t -> Term.t -> unit
      type config = Partition.t * t
      val update : config -> Fact.Equal.t -> unit
      val diff : t -> t -> t
      val copy : t -> t
    end
  type tag = R | T
  val pp : La.tag -> La.S.t Pretty.printer
  val can : Partition.t * La.S.t -> Jst.Eqtrans.t
  val nl_merge : (Fact.Equal.t -> unit) Pervasives.ref
  module Infsys :
    sig
      type e = S.t
      val current : unit -> e
      val initialize : e -> unit
      val finalize : unit -> e
      val abstract : Term.t -> unit
      val merge : Fact.Equal.t -> unit
      val propagate : Fact.Equal.t -> unit
      val dismerge : Fact.Diseq.t -> unit
      val propagate_diseq : Fact.Diseq.t -> unit
      val branch : unit -> unit
      val normalize : unit -> unit
      val nonneg : Fact.Nonneg.t -> unit
      val pos : Fact.Pos.t -> unit
    end
  exception Unbounded
  val upper : Partition.t * La.S.t -> Jst.Eqtrans.t
  val lower : Partition.t * La.S.t -> Jst.Eqtrans.t
  val is_equal : Partition.t * La.S.t -> Jst.Pred2.t
  val model : La.S.t -> Term.t list -> Term.t Term.Map.t
end