Kernel: Optimise conversion

[francoisthire]

Partial answer to #279 .

1. We add a physical equality for optimisation. We can check this may be triggered by some unit tests
2. We still keep the syntactic equality. This is to avoid to compute the WHNF while to terms are syntactically equal (see test : tests/OK/sharing.dk).

[01mf02]

How about just checking for physical equality as part of term_eq?
This has two advantages:

1. It would likely accelerate other sites where term_eq is currently called without checking for physical equality, for example in srcheck.ml.
2. If you have two terms that are not physically equal, but their subterms are, then checking for physical equality in the recursive calls of term_eq would make term_eq faster.