Adapt to Coq PR #17832: syntax of choice in rewstrategy expects arguments at atomic level

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

https://math-classes.github.io

MIT License

162 stars 43 forks source link

Closed herbelin closed 1 year ago

herbelin commented 1 year ago

The PR is necessary to be compatible with the Coq PR coq/coq#17832 but if the patch is ok for you, this can be merged as soon as now.

PS: There are spaces in ( <- associativity ) to prevent the notation (< x ) to be parsed instead.

JasonGross commented 1 year ago

@spitters does this patch look good? Can this be merged?