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).
Last updated: Nov 29 2023 at 22:01 UTC