aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2020-02-14 23:48:57 +0100
committerPierre-Marie Pédrot2020-02-14 23:48:57 +0100
commit4de476c53d85be4dd266cfe5fd5f2ddec9163a5b (patch)
tree1f8cb4ea4350ee9dfef0d65a90aebdd3d939c1d5 /dev
parentbdc8e29d806ab7e9bbd0491bf237890b7934795a (diff)
parent0f58738351db02f30ac43ec52517c54b315d5886 (diff)
Merge PR #11557: Use thunks to univ instead of lazy constr for template typing
Reviewed-by: ppedrot
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh12
1 files changed, 12 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh
new file mode 100644
index 0000000000..913b39c30c
--- /dev/null
+++ b/dev/ci/user-overlays/11557-SkySkimmer-template-directify.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "11557" ] || [ "$CI_BRANCH" = "template-directify" ]; then
+
+ equations_CI_REF=template-directify
+ equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+ paramcoq_CI_REF=template-directify
+ paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+ elpi_CI_REF=template-directify
+ elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi