[ssreflect] Use rw instead of rewrite to avoid conflicts with legacy tactic #21478
+1,363
−1,217
coqbot-app / GitLab CI job doc:ci-refman (pull request)
failed
Mar 9, 2026 in 0s
Test has failed on GitLab CI
This job has failed. If you need to, you can restart it directly in the GitHub interface using the "Re-run" button.
This job ran on the Docker image registry.gitlab.inria.fr/coq/coq:edge_ubuntu-V2026-03-04-d4fe8f0464 with OCaml 4.14.2+flambda and depended on jobs build:edge+flambda library:ci-mathcomp library:ci-mczify library:ci-stdlib+flambda plugin:ci-elpi_hb. It built targets refman.
We show below an excerpt from the trace from GitLab starting around the last detected "Error" (the complete trace is available here).
Details
File "plugins/ssrrewrite/ssrrewrite.mlg", line 13, characters 0-10:
Error (warning 33 [unused-open]): unused open Names.
Running after_script
Running after script...
$ if { [ "$SAVE_BUILD_CI" ] || [ "$CI_COMMIT_REF_NAME" = master ] || ! [ -e ci-success ]; } && [ -d _build_ci ]; then mv _build_ci saved_build_ci; fi
$ dev/tools/list-potential-artifacts.sh > available_artifacts.txt
$ dev/tools/cleanup-artifacts.sh downloaded_artifacts.txt available_artifacts.txt
Uploading artifacts for failed job
Uploading artifacts...
_build/log: found 1 matching artifact files and directories
WARNING: _build/default/doc/refman-html: no matching files. Ensure that the artifact path is relative to the working directory (/builds/coq/coq)
WARNING: _build/default/doc/refman-pdf: no matching files. Ensure that the artifact path is relative to the working directory (/builds/coq/coq)
Uploading artifacts as "archive" to coordinator... 201 Created correlation_id=01KK8X5XFEAG4ZFEBYGBV2JNNZ id=6972912 responseStatus=201 Created token=64_znPhHs
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1
Loading