Towards a better-behaved unification algorithm for Coq

ABSTRACT. 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 who has to fill implicit terms and missing type annotations), and the application of lemmas. Despite of being so important, however, the current unification algorithm of Coq is not properly documented, and implements certain heuristics that makes unification unpredictable and hard to understand.

In this work we discuss some of the problems with the current algorithm and present a new one, built from scratch, which aims at solving these issues. The new algorithm is properly documented, putting us on better grounds for a formally verified and optimized algorithm.