Adapting `ci-coq_library_undecidability`

for https://github.com/coq/coq/pull/17538 unfortunately broke the current Coq CI.

If https://github.com/coq/coq/pull/17538 is merged soon, then there is no problem.

Otherwise, we need some intermediate solution.

We should just merge #17538. But if you want a backwards compatible change, you can do a hack like replacing `tmExistingInstance global (ConstRef name)`

with `ltac:(eapply tmExistingInstance; try exact (ConstRef name); constructor <whichever number global is>)`

Just merging #17538 is fine. The policy of `coq_library_undecidability`

is to be compatible with a specific Coq version (and avoid legacy glue code).

merged

Last updated: Oct 13 2024 at 01:02 UTC