Towards a better-behaved unification algorithm for Coq

The unification algorithm is at the heart of a proof assistant like Coq. In particular, it is a key component in the refiner (the algorithm that has to infer implicit terms and missing type annotations) and in the ap-plication of lemmas. In the first case, unification is in charge of equating the type of function arguments with the type of the elements to which the function is applied. In the second case, for instance whe