aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/user-overlays/11235-non-maximal-implicit.sh31
1 files changed, 0 insertions, 31 deletions
diff --git a/dev/ci/user-overlays/11235-non-maximal-implicit.sh b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
index dc4fdd48de..fd63980036 100644
--- a/dev/ci/user-overlays/11235-non-maximal-implicit.sh
+++ b/dev/ci/user-overlays/11235-non-maximal-implicit.sh
@@ -6,35 +6,4 @@ if [ "$CI_PULL_REQUEST" = "11235" ] || [ "$CI_BRANCH" = "non-maximal-implicit" ]
elpi_CI_REF=non_maximal_implicit
elpi_CI_GITURL=https://github.com/SimonBoulier/coq-elpi
- # the following are also in 11368-trailing-implicit-error.sh
- mathcomp_CI_REF=non_maximal_implicit
- mathcomp_CI_GITURL=https://github.com/SimonBoulier/math-comp
-
- oddorder_CI_REF=non_maximal_implicit
- oddorder_CI_GITURL=https://github.com/SimonBoulier/odd-order
-
- stdlib2_CI_REF=non_maximal_implicit
- stdlib2_CI_GITURL=https://github.com/SimonBoulier/stdlib2
-
- coq_dpdgraph_CI_REF=non_maximal_implicit
- coq_dpdgraph_CI_GITURL=https://github.com/SimonBoulier/coq-dpdgraph
-
- vst_CI_REF=non_maximal_implicit
- vst_CI_GITURL=https://github.com/SimonBoulier/VST
-
- equations_CI_REF=non_maximal_implicit
- equations_CI_GITURL=https://github.com/SimonBoulier/Coq-Equations
-
- mtac2_CI_REF=non_maximal_implicit
- mtac2_CI_GITURL=https://github.com/SimonBoulier/Mtac2
-
- relation_algebra_CI_REF=non_maximal_implicit
- relation_algebra_CI_GITURL=https://github.com/SimonBoulier/relation-algebra
-
- fiat_parsers_CI_REF=non_maximal_implicit
- fiat_parsers_CI_GITURL=https://github.com/SimonBoulier/fiat
-
- Corn_CI_REF=non_maximal_implicit
- Corn_CI_GITURL=https://github.com/SimonBoulier/corn
-
fi