Skip to content

Commit 896484b

Browse files
cuihtlauacclaude
andcommitted
Fix Rocq build: remove rocq-extraction (bundled in rocq-stdlib)
Extraction support is included via rocq-stdlib, which rocq-prover already depends on. The rocq-extraction package does not exist in opam. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 078ac4e commit 896484b

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

rocq/Dockerfile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -24,7 +24,7 @@ WORKDIR /home/vscode
2424
RUN opam switch ocaml && \
2525
eval $(opam env) && \
2626
opam update && \
27-
opam install -y rocq-prover rocq-extraction
27+
opam install -y rocq-prover
2828

2929
# ============================================================================
3030
# Cleanup

0 commit comments

Comments
 (0)