Kazuhiko Sakaguchi

IIRC, the `zify` tactic supports only first-order terms and thus does not support polymorphic types (such as products) and parametric instances (such as `Op_eqb_pair`). I guess reimplementing `zify` in Coq-elpi...

@gares I don't think letting the user specify this number for every tactic call is very useful. If I should make it configurable, I would do that through a tactic...

The actual code that requires this fuel is, I guess, these functions in `setoid_ring`: https://github.com/coq/coq/blob/110921a449fcb830ec2a1cd07e3acc32319feae6/theories/setoid_ring/Ring_polynom.v#L467-L499 I'm not going to change them. But, it seems to me that [`(10*10*10)%nat`](https://github.com/coq/coq/blob/110921a449fcb830ec2a1cd07e3acc32319feae6/theories/setoid_ring/Ring_tac.v#L340) is an...

> is this the code that handles the substitution of `H1` in `ring [H1]`? Yes, I think so, and my main problem is that I have no idea how big...

If the goal is implication `P1 -> ... -> Pn -> Q`, my `ring` tactic uses `P1 ... Pn` as assumptions.

Aha, I thought it was more intelligent. I will try to produce such an example.

@gares I think now I need to do the same for the second item of https://github.com/math-comp/algebra-tactics/pull/22#issuecomment-935858368, and it would be nice if we can set/unset these options globally. Do you...

@gares Thanks. That's indeed desirable.

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

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...