- equality test on terms before trying convertibility now first tries
phyisical equality between terms and then fallback to structural
equality (same behaviour of ocaml < 3.08)
- changed behaviour of are_convertible. Before this change: equality was
first tried on terms (as above) then, in case of failure, equality
between weak head reduced terms was tried. Now weak head reduction is
always performed. This change is motivated by the convertibility
between "sin x" and "cos x" (no one was able to see the end of this
test case). Now this test case completes almost immediately and
regression test type checking the whole standard library does not
shown any sensible slow down