Is there some documentation for the different unification types defined in pattern.v, namely
=> UniMatch =n> UniMatchNoRed =u> UniCoq =c> UniEvarConv
I can imagine what UniMatchNoRed does - I guess it behaves similar to a match in Ltac1 - but the difference between the others is not obvious from the name.
There is a lot of other syntax in pattern.v which I am convinced serves some very useful purpose, but it is really hard to tell which.
Maybe they use unification (apply:)/tactic unification (apply) / unicoq unification?
EvarConv is one of the unification algorithms, after all.
(IIRC it’s the one in ssreflect, but this zulip has authoritative answers)
https://mattermost.mpi-sws.org/iris/pl/hd1pguiz1bbdxgnkq99qswrixo and discussion around seems to confirm your guess for UniMatchNoRed.
Sorry, forgot to reply to this thread. @Beta Ziliani is the expert but my current understanding is this:
*Match* implies that the pattern will not try to instantiate evars in the value it is compared against. The two different
Match differ in how much reduction they perform in the value (but they never reduce in the pattern, IIRC.).
UniCoq is full unification with the unicoq algorithm, including reduction and evar instantiation on both sides (pattern and value).
UniEvarconv is the same but with Coq's own unification algorithm.
this is correct
Last updated: Feb 06 2023 at 05:03 UTC