functor
  (T : sig
         type t
         type elt
         val empty : Unification.t
         val is_empty : Unification.t -> bool
         val equal : Unification.t -> Unification.t -> bool
         val add : Unification.elt -> Unification.t -> Unification.t
         val choose : Unification.t -> Unification.elt
         val remove : Unification.elt -> Unification.t -> Unification.t
         val find_map :
           (Unification.elt -> 'a option) -> Unification.t -> 'a option
       end) ->
  sig
    val mk_unifier :
      bool ->
      bool ->
      (T.elt -> T.elt -> ('a -> 'b option) -> 'a -> 'b option) ->
      T.t -> T.t -> ('a -> 'b option) -> 'a -> 'b option
  end