sig
  module type SIG = sig val th : Th.t val f : Sym.t end
  module type TERM =
    sig
      val d_interp : Term.t -> Term.t * Term.t
      val is_interp : Term.t -> bool
      val make : Term.t -> Term.t -> Term.t
      val iterate : Term.t -> int -> Term.t
      val multiplicity : Term.t -> Term.t -> int
      val decompose : Term.t -> (Term.t * int) * Term.t option
      val fold : (Term.t -> int -> 'a -> 'a) -> Term.t -> 'a -> 'a
      val iter : (Term.t -> int -> unit) -> Term.t -> unit
      val sigma : Sym.t -> Term.t list -> Term.t
      val map : (Term.t -> Term.t) -> Term.t -> Term.t
    end
  module Ops : functor (Sig : SIG) -> Can.OPS
  module Make : functor (Sig : SIG) -> TERM
  module T : functor (Sig : SIG) -> Can.T
  module Infsys :
    functor (Sig : SIG) ->
      sig
        type e = Solution.Set.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
      end
end