1. The equality symbol is now bidirectionally compatible with coercions.
That is, in the  module Binary below (see bench/typing/good/coercions.mlw),
goal G is well-typed, with coercion [to_int] being applied to variable [x]
both in [x=y] and in [y=x] :

module Binary

  use import int.Int
  use import mach.int.Int63

  goal G: forall x: int63, y: int. x = y /\ y = x

end

2. Each coercion is still uniquely defined by type symbols [Ts, Ts']

   [ ls: Ts1 ty_1,1 ... ty_1,n -> Ts2 ty_2,1 ... ty_2,m ],

but searching for a possible coercion is now taking into account
types [ ty_1,1 ... ty_1,n ] and [ ty_2,1 ... ty_2,m ] in order to
compare them with the actual type of a term [t] on which coercion may
apply as well as the actual expected type.

(That is, now the signature of find is [t -> ty -> ty -> lsymbol list])

This is done to anticipate in a heurstic way a situation when
a coercion can be technically applied but will eventually fail, because
type mismatch between types in coercion signature and the types of
a term on which coercion applies. For instance, given a coercion

  function to_list bool : list bool
  meta coercion function to_list

the following goal is rejected by typing:

  goal G: forall x: list int, y: bool.  x = y

Indeed, [y] is expected to be of type [list int].
Since [y] is of type [bool], one may try to apply a coercion [to_list]
in order to get a term [to_list y] of type [list bool].
However, this would not help, since a [list bool] mismatch with [list int].

The error message is now better:

"This term (i.e. [y]) has type bool, but is expected to have type list int"

compared to old version:

"This term  (i.e. [y])  has type list bool, but is expected to have type list int"