Skip to content

Hide definition of tacvalue in tacinterp

b6528af
Select commit
Loading
Failed to load commit list.
Open

wit_tactic top type is tacvalue #21680

Hide definition of tacvalue in tacinterp
b6528af
Select commit
Loading
Failed to load commit list.
coqbot-app / GitLab CI job plugin:ci-elpi_hb (pull request) failed Mar 5, 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. It built targets elpi hb.

We show below an excerpt from the trace from GitLab starting around the last detected "Error" (the complete trace is available here).

Details

                               ^^^
Error: This expression has type Tacinterp.value
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...
WARNING: _install_ci: no matching files. Ensure that the artifact path is relative to the working directory (/builds/coq/coq) 
saved_build_ci: found 1573 matching artifact files and directories 
saved_build_ci/**/.git: excluded 1 files           
Uploading artifacts as "archive" to coordinator... 201 Created  correlation_id=01KJZMKQEHYWSWK61TE0BWAB5E id=6959919 responseStatus=201 Created token=64_ZkA9E_
Cleaning up project directory and file based variables
ERROR: Job failed: exit code 1