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):
- In what situations are each of these unification algorithms used?
- What differences can we observe between the two algorithms?
- Are there any tricks to force one algorithm over the other as the situation may require?
- 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.