Could I get review / an assignee on #17938 (adjusting the infrastructure in the test-suite file for `nia`

a bit, in prep for handling more test cases). (#17933 is the PR that actually adds the extra test-cases, and #17934 (more power in Z.to_euclidean_division_equations) also depends on #17938)

What is the status of https://github.com/coq/coq/pull/17920? It is a PR fixing a regression in 8.18 over 8.17 that I prepared before 8.18.0 was tagged, but which was not merged in time...

Is anyone willing to be assignee on https://github.com/coq/coq/pull/18094 (exposing the fixpoint operator in `rewrite_strat`

?)

There's also a question about the right way to parse/intern `constr_or_var`

in `plugins/ltac/tacintern.ml`

in the PR.

I'm not saying that this is the "right" way to do, but it is common in Ltac1 internals to encode bound variables in constr nodes. In any case, the way you did in the PR is ok to me.

Last updated: Oct 13 2024 at 01:02 UTC