Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 0 additions & 6 deletions .gitlab-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -1166,12 +1166,6 @@ plugin:ci-mtac2:
- build:edge+flambda
- library:ci-stdlib+flambda

plugin:ci-paramcoq:
extends: .ci-template-flambda
needs:
- build:edge+flambda
- library:ci-stdlib+flambda

plugin:ci-perennial:
extends: .ci-template-flambda
needs:
Expand Down
3 changes: 0 additions & 3 deletions Makefile.ci
Original file line number Diff line number Diff line change
Expand Up @@ -33,7 +33,6 @@ CI_PLATFORM_FULL= \
ci-analysis \
ci-menhir \
ci-mtac2 \
ci-paramcoq \
ci-quickchick \
ci-reduction_effects \
ci-relation_algebra \
Expand Down Expand Up @@ -224,8 +223,6 @@ ci-vst: ci-compcert

ci-compcert: ci-menhir ci-flocq

ci-paramcoq: ci-stdlib

ci-perennial: ci-stdlib

ci-aac_tactics: ci-stdlib
Expand Down
6 changes: 0 additions & 6 deletions dev/ci/ci-basic-overlay.sh
Original file line number Diff line number Diff line change
Expand Up @@ -386,12 +386,6 @@ project async_test "https://github.com/liyishuai/coq-async-test" "master"
project http "https://github.com/liyishuai/coq-http" "master"
# Contact @liyishuai on github

########################################################################
# paramcoq
########################################################################
project paramcoq "https://github.com/coq-community/paramcoq" "master"
# Contact @proux01 on github

########################################################################
# relation_algebra
########################################################################
Expand Down
17 changes: 0 additions & 17 deletions dev/ci/ci-paramcoq.sh

This file was deleted.

2 changes: 1 addition & 1 deletion vernac/assumptions.mli
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ open Printer
sealed inside opaque modules. Do not try to do anything fancy with those
terms apart from printing them, otherwise demons may fly out of your nose.

NOTE: this function is used in the plugin paramcoq.
NOTE: this function was used in the plugin paramcoq (which no longer exists).
*)
val traverse :
Global.indirect_accessor -> Label.t -> constr ->
Expand Down