Compare variables by conversion or keyed matching

[pi8027]

Although it may lead to some performance issues.

[gares]

you can pass the tactic an option in that case

[pi8027]

@gares I think now I need to do the same for the second item of #22 (comment), and it would be nice if we can set/unset these options globally. Do you think it is possible?

[gares]

Hum, one thing I could do is to let one access the option tables you can alter with [Un]Set FooBar [int|string] but it is a bit unclear to me how to make one register options here... I mean, it should be done only once and in one place... I'll have to check if this is possible.

[pi8027]

@gares Thanks. That's indeed desirable.

[pi8027]

It seems to me that this feature will be useful in apery. https://github.com/math-comp/apery/blob/c484e1f869526b78a81f0a10e1a657096eac35bb/theories/field_tactics.v#L198-L205

[pi8027]

Before addressing this issue, I wish to have a cache mechanism for conversion checking (based on union-find). That would also apply to the comparisons of instances and reduce the time spent on readback.