aboutsummaryrefslogtreecommitdiff
path: root/dev/ci/user-overlays
diff options
context:
space:
mode:
Diffstat (limited to 'dev/ci/user-overlays')
-rw-r--r--dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh15
-rw-r--r--dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh6
-rw-r--r--dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh24
-rw-r--r--dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh15
-rw-r--r--dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh6
5 files changed, 66 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
new file mode 100644
index 0000000000..e3a8eb07f3
--- /dev/null
+++ b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then
+
+ metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+ metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
+
+ elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+ elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+ paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+ paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+ equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+ equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh
new file mode 100644
index 0000000000..4170799be7
--- /dev/null
+++ b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11820" ] || [ "$CI_BRANCH" = "partial-import" ]; then
+
+ elpi_CI_REF=partial-import
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
new file mode 100644
index 0000000000..cd6b408813
--- /dev/null
+++ b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
@@ -0,0 +1,24 @@
+if [ "$CI_PULL_REQUEST" = "11896" ] || [ "$CI_BRANCH" = "evar-inst-list" ]; then
+
+ coqhammer_CI_REF="evar-inst-list"
+ coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
+
+ elpi_CI_REF="evar-inst-list"
+ elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+ equations_CI_REF="evar-inst-list"
+ equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+ metacoq_CI_REF="evar-inst-list"
+ metacoq_CI_GITURL=https://github.com/ppedrot/metacoq
+
+ mtac2_CI_REF="evar-inst-list"
+ mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+ quickchick_CI_REF="evar-inst-list"
+ quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
+
+ unicoq_CI_REF="evar-inst-list"
+ unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+fi
diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
new file mode 100644
index 0000000000..6bee3c7bb6
--- /dev/null
+++ b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then
+
+ fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+ fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto
+
+ mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+ mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
+
+ metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+ metacoq_CI_GITURL=https://github.com/herbelin/template-coq
+
+ unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+ unimath_CI_GITURL=https://github.com/herbelin/UniMath
+
+fi
diff --git a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
new file mode 100644
index 0000000000..b5faabcfe1
--- /dev/null
+++ b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12107" ] || [ "$CI_BRANCH" = "no-mod-univs" ]; then
+
+ elpi_CI_REF=no-mod-univs
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi