sig
  type scope = LogtkSubsts.scope
  type subst = LogtkSubsts.t
  type env = LogtkScopedTerm.t LogtkDBEnv.t
  type 'a sequence = ('-> unit) -> unit
  type res = LogtkUnif.subst LogtkUnif.sequence
  val res_head : LogtkUnif.res -> LogtkUnif.subst option
  exception Fail
  module type UNARY =
    sig
      type term
      val unification :
        ?env1:LogtkUnif.env ->
        ?env2:LogtkUnif.env ->
        ?subst:LogtkUnif.subst ->
        LogtkUnif.UNARY.term ->
        LogtkUnif.scope ->
        LogtkUnif.UNARY.term -> LogtkUnif.scope -> LogtkUnif.subst
      val matching :
        ?allow_open:bool ->
        ?env1:LogtkUnif.env ->
        ?env2:LogtkUnif.env ->
        ?subst:LogtkUnif.subst ->
        pattern:LogtkUnif.UNARY.term ->
        LogtkUnif.scope ->
        LogtkUnif.UNARY.term -> LogtkUnif.scope -> LogtkUnif.subst
      val matching_same_scope :
        ?env1:LogtkUnif.env ->
        ?env2:LogtkUnif.env ->
        ?protect:LogtkUnif.UNARY.term Sequence.t ->
        ?subst:LogtkUnif.subst ->
        scope:LogtkUnif.scope ->
        pattern:LogtkUnif.UNARY.term ->
        LogtkUnif.UNARY.term -> LogtkUnif.subst
      val matching_adapt_scope :
        ?env1:LogtkUnif.env ->
        ?env2:LogtkUnif.env ->
        ?protect:LogtkUnif.UNARY.term Sequence.t ->
        ?subst:LogtkUnif.subst ->
        pattern:LogtkUnif.UNARY.term ->
        LogtkUnif.scope ->
        LogtkUnif.UNARY.term -> LogtkUnif.scope -> LogtkUnif.subst
      val variant :
        ?env1:LogtkUnif.env ->
        ?env2:LogtkUnif.env ->
        ?subst:LogtkUnif.subst ->
        LogtkUnif.UNARY.term ->
        LogtkUnif.scope ->
        LogtkUnif.UNARY.term -> LogtkUnif.scope -> LogtkUnif.subst
      val eq :
        ?env1:LogtkUnif.env ->
        ?env2:LogtkUnif.env ->
        subst:LogtkUnif.subst ->
        LogtkUnif.UNARY.term ->
        LogtkUnif.scope -> LogtkUnif.UNARY.term -> LogtkUnif.scope -> bool
      val are_unifiable :
        LogtkUnif.UNARY.term -> LogtkUnif.UNARY.term -> bool
      val matches :
        pattern:LogtkUnif.UNARY.term -> LogtkUnif.UNARY.term -> bool
      val are_variant : LogtkUnif.UNARY.term -> LogtkUnif.UNARY.term -> bool
    end
  module type NARY =
    sig
      type term
      type result = LogtkUnif.res
      val unification :
        ?env1:LogtkUnif.env ->
        ?env2:LogtkUnif.env ->
        ?subst:LogtkUnif.subst ->
        LogtkUnif.NARY.term ->
        LogtkUnif.scope ->
        LogtkUnif.NARY.term -> LogtkUnif.scope -> LogtkUnif.NARY.result
      val matching :
        ?allow_open:bool ->
        ?env1:LogtkUnif.env ->
        ?env2:LogtkUnif.env ->
        ?subst:LogtkUnif.subst ->
        pattern:LogtkUnif.NARY.term ->
        LogtkUnif.scope ->
        LogtkUnif.NARY.term -> LogtkUnif.scope -> LogtkUnif.NARY.result
      val variant :
        ?env1:LogtkUnif.env ->
        ?env2:LogtkUnif.env ->
        ?subst:LogtkUnif.subst ->
        LogtkUnif.NARY.term ->
        LogtkUnif.scope ->
        LogtkUnif.NARY.term -> LogtkUnif.scope -> LogtkUnif.NARY.result
      val are_unifiable : LogtkUnif.NARY.term -> LogtkUnif.NARY.term -> bool
      val matches :
        pattern:LogtkUnif.NARY.term -> LogtkUnif.NARY.term -> bool
      val are_variant : LogtkUnif.NARY.term -> LogtkUnif.NARY.term -> bool
    end
  module Nary :
    sig
      type term = LogtkScopedTerm.t
      type result = res
      val unification :
        ?env1:env ->
        ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> result
      val matching :
        ?allow_open:bool ->
        ?env1:env ->
        ?env2:env ->
        ?subst:subst -> pattern:term -> scope -> term -> scope -> result
      val variant :
        ?env1:env ->
        ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> result
      val are_unifiable : term -> term -> bool
      val matches : pattern:term -> term -> bool
      val are_variant : term -> term -> bool
    end
  module Unary :
    sig
      type term = LogtkScopedTerm.t
      val unification :
        ?env1:env ->
        ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> subst
      val matching :
        ?allow_open:bool ->
        ?env1:env ->
        ?env2:env ->
        ?subst:subst -> pattern:term -> scope -> term -> scope -> subst
      val matching_same_scope :
        ?env1:env ->
        ?env2:env ->
        ?protect:term Sequence.t ->
        ?subst:subst -> scope:scope -> pattern:term -> term -> subst
      val matching_adapt_scope :
        ?env1:env ->
        ?env2:env ->
        ?protect:term Sequence.t ->
        ?subst:subst -> pattern:term -> scope -> term -> scope -> subst
      val variant :
        ?env1:env ->
        ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> subst
      val eq :
        ?env1:env ->
        ?env2:env -> subst:subst -> term -> scope -> term -> scope -> bool
      val are_unifiable : term -> term -> bool
      val matches : pattern:term -> term -> bool
      val are_variant : term -> term -> bool
    end
  module Ty :
    sig
      type term = LogtkType.t
      val unification :
        ?env1:env ->
        ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> subst
      val matching :
        ?allow_open:bool ->
        ?env1:env ->
        ?env2:env ->
        ?subst:subst -> pattern:term -> scope -> term -> scope -> subst
      val matching_same_scope :
        ?env1:env ->
        ?env2:env ->
        ?protect:term Sequence.t ->
        ?subst:subst -> scope:scope -> pattern:term -> term -> subst
      val matching_adapt_scope :
        ?env1:env ->
        ?env2:env ->
        ?protect:term Sequence.t ->
        ?subst:subst -> pattern:term -> scope -> term -> scope -> subst
      val variant :
        ?env1:env ->
        ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> subst
      val eq :
        ?env1:env ->
        ?env2:env -> subst:subst -> term -> scope -> term -> scope -> bool
      val are_unifiable : term -> term -> bool
      val matches : pattern:term -> term -> bool
      val are_variant : term -> term -> bool
    end
  module FO :
    sig
      type term = LogtkFOTerm.t
      val unification :
        ?env1:env ->
        ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> subst
      val matching :
        ?allow_open:bool ->
        ?env1:env ->
        ?env2:env ->
        ?subst:subst -> pattern:term -> scope -> term -> scope -> subst
      val matching_same_scope :
        ?env1:env ->
        ?env2:env ->
        ?protect:term Sequence.t ->
        ?subst:subst -> scope:scope -> pattern:term -> term -> subst
      val matching_adapt_scope :
        ?env1:env ->
        ?env2:env ->
        ?protect:term Sequence.t ->
        ?subst:subst -> pattern:term -> scope -> term -> scope -> subst
      val variant :
        ?env1:env ->
        ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> subst
      val eq :
        ?env1:env ->
        ?env2:env -> subst:subst -> term -> scope -> term -> scope -> bool
      val are_unifiable : term -> term -> bool
      val matches : pattern:term -> term -> bool
      val are_variant : term -> term -> bool
    end
  module HO :
    sig
      type term = LogtkHOTerm.t
      type result = res
      val unification :
        ?env1:env ->
        ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> result
      val matching :
        ?allow_open:bool ->
        ?env1:env ->
        ?env2:env ->
        ?subst:subst -> pattern:term -> scope -> term -> scope -> result
      val variant :
        ?env1:env ->
        ?env2:env -> ?subst:subst -> term -> scope -> term -> scope -> result
      val are_unifiable : term -> term -> bool
      val matches : pattern:term -> term -> bool
      val are_variant : term -> term -> bool
    end
  module Form :
    sig
      val variant :
        ?env1:LogtkUnif.env ->
        ?env2:LogtkUnif.env ->
        ?subst:LogtkUnif.subst ->
        LogtkFormula.FO.t ->
        LogtkUnif.scope ->
        LogtkFormula.FO.t -> LogtkUnif.scope -> LogtkUnif.res
      val are_variant : LogtkFormula.FO.t -> LogtkFormula.FO.t -> bool
    end
end