sig
  type t
  val empty : Coercion.t
  val add : Coercion.t -> Why3.Term.lsymbol -> Coercion.t
  val find : Coercion.t -> Why3.Ty.ty -> Why3.Ty.ty -> Why3.Term.lsymbol list
  val union : Coercion.t -> Coercion.t -> Coercion.t
end