I gather, from practical experience and Zulip hearsay, that Coq has two unification algorithms, known as “tactic unification” and “evarconv”. However, I can't find any documentation on these from a web search.

I would like to know (with 3 and 4 being optional):

  1. In what situations are each of these unification algorithms used?
  2. What differences can we observe between the two algorithms?
  3. Are there any tricks to force one algorithm over the other as the situation may require?
  4. How do both algorithms compare to those of other dependently typed programming languages? I'm most familiar with Agda, but I think any comparison could help me understand the scope of unification in Coq.
  • 3
    $\begingroup$ Are you aware of doi.org/10.1145/2784731.2784751 and doi.org/10.1017/S0956796817000028 ? $\endgroup$ Apr 30 at 18:13
  • $\begingroup$ @AndrejBauer I don't think I was. Which unification algorithm(s) do they refer to? $\endgroup$
    – mudri
    May 1 at 9:54
  • $\begingroup$ I am not following too closely, but I think that's the new one that is implemented in the latest versions of Coq. If Pierre-Marie walks by he can tell for sure. $\endgroup$ May 1 at 10:01


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.