sig
  type symbol = int
  type var = int
  type units = (Matcher.symbol * Matcher.symbol) list
  type ext_units = {
    unit_for : Matcher.units;
    is_ac : (Matcher.symbol * bool) list;
  }
  type 'a mset = ('a * int) list
  val linear : 'a Matcher.mset -> 'a list
  module Terms :
    sig
      type t =
          Dot of (Matcher.symbol * Matcher.Terms.t * Matcher.Terms.t)
        | Plus of (Matcher.symbol * Matcher.Terms.t * Matcher.Terms.t)
        | Sym of (Matcher.symbol * Matcher.Terms.t array)
        | Var of Matcher.var
        | Unit of Matcher.symbol
      val equal_aac :
        Matcher.units -> Matcher.Terms.t -> Matcher.Terms.t -> bool
      val map_syms :
        (Matcher.symbol -> Matcher.symbol) ->
        Matcher.Terms.t -> Matcher.Terms.t
      type nf_term
      val nf_term_compare :
        Matcher.Terms.nf_term -> Matcher.Terms.nf_term -> int
      val nf_equal : Matcher.Terms.nf_term -> Matcher.Terms.nf_term -> bool
      val sprint_nf_term : Matcher.Terms.nf_term -> string
      val term_of_t :
        Matcher.units -> Matcher.Terms.t -> Matcher.Terms.nf_term
      val t_of_term : Matcher.Terms.nf_term -> Matcher.Terms.t
    end
  module Subst :
    sig
      type t
      val sprint : Matcher.Subst.t -> string
      val instantiate : Matcher.Subst.t -> Matcher.Terms.t -> Matcher.Terms.t
      val to_list : Matcher.Subst.t -> (Matcher.var * Matcher.Terms.t) list
    end
  val matcher :
    ?strict:bool ->
    Matcher.ext_units ->
    Matcher.Terms.t -> Matcher.Terms.t -> Matcher.Subst.t Search_monad.m
  val subterm :
    ?strict:bool ->
    Matcher.ext_units ->
    Matcher.Terms.t ->
    Matcher.Terms.t ->
    (int * Matcher.Terms.t * Matcher.Subst.t Search_monad.m) Search_monad.m
end