Registering strict implicit arguments systematically.
Experimenting always forcing convertibility on strict implicit arguments
in tactic unification.