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/12611-ejgallego-record+refactor.sh9
-rw-r--r--dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh15
-rw-r--r--dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh6
3 files changed, 30 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh
new file mode 100644
index 0000000000..b7d21ed59c
--- /dev/null
+++ b/dev/ci/user-overlays/12611-ejgallego-record+refactor.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "12611" ] || [ "$CI_BRANCH" = "record+refactor" ]; then
+
+ elpi_CI_REF=record+refactor
+ elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+# mtac2_CI_REF=record+refactor
+# mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+fi
diff --git a/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh b/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh
new file mode 100644
index 0000000000..1473f6df8b
--- /dev/null
+++ b/dev/ci/user-overlays/12653-SkySkimmer-cumul-syntax.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "12653" ] || [ "$CI_BRANCH" = "cumul-syntax" ]; then
+
+ overlay elpi https://github.com/SkySkimmer/coq-elpi cumul-syntax
+
+ overlay equations https://github.com/SkySkimmer/Coq-Equations cumul-syntax
+
+ overlay mtac2 https://github.com/SkySkimmer/Mtac2 cumul-syntax
+
+ overlay paramcoq https://github.com/SkySkimmer/paramcoq cumul-syntax
+
+ overlay rewriter https://github.com/SkySkimmer/rewriter cumul-syntax
+
+ overlay metacoq https://github.com/SkySkimmer/metacoq cumul-syntax
+
+fi
diff --git a/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh b/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh
new file mode 100644
index 0000000000..7680e8da78
--- /dev/null
+++ b/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12873" ] || [ "$CI_BRANCH" = "master+minifix-unification-error-reporting-recheck-applications" ]; then
+
+ equations_CI_REF=master+fix12873-better-unification
+ equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi