Questions tagged [unification]

Unification is a technique used in the implementation of proof assistants for purposes including solving of metavariables and resolution of type classes.

Filter by
Sorted by
Tagged with
2 votes
0 answers

SSReflect tuple constructor: why not use phantom?

I was reading the mathcomp book learning about canonical structures and following along with the mathcomp source to compare how things were done in practice. Specifically I was looking at sections 6....
user avatar
4 votes
0 answers

Tactic unification vs evarconv in Coq

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 ...
user avatar
  • 497