In dest_prod_assum, allow non-toplevel let-reductions (fixes a bug found in MathClasses).
Missing check of evar instantiation, resulting in missing constraints (bug from MathClasses).
In flex-flex cases, the undefinedness of an evar can not be preseved after converting
the stacks. Take care of this by recalling unification.