Change (or better define) the order of hints premises.

Change (or better define) the order of hints premises.

They are now processed top to bottom, and not viceversa as before. This seems
to be right thing, since rules like:

  X := carr T
  ....
  R := mk_foo ... (P X) ... T ...
 --------------------------------- |-
  carr R = (P X)

can't be written putting X := carr T last, but you really want to be sure that
the needed assumptions to obtain a foo (in that case, that X is the carrier of
a setoid T) are available _before_ you even try to typecheck the bigger
unification problem (that may not be well typed if X and carr T are not
_convertible_, since in the fix function called in instantiate we call the
typechecker and not the refiner).