aboutsummaryrefslogtreecommitdiff
path: root/dev/ci
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2019-06-25 17:26:44 +0200
committerPierre-Marie Pédrot2019-06-25 17:26:44 +0200
commit7dfcb0f7c817e66280ab37b6c653b5596a16c249 (patch)
treef59cbad4ef2e56070fe32fefcc5f7a3f8c6b7a4a /dev/ci
parent7024688c4e20fa7b70ac1c550c166d02fce8d15c (diff)
parentc2abcaefd796b7f430f056884349b9d959525eec (diff)
Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.
Reviewed-by: SkySkimmer Ack-by: ejgallego Reviewed-by: gares Reviewed-by: ppedrot
Diffstat (limited to 'dev/ci')
-rw-r--r--dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh18
1 files changed, 18 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh b/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh
new file mode 100644
index 0000000000..d133bc9993
--- /dev/null
+++ b/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "10316" ] || [ "$CI_BRANCH" = "proof+recthms" ]; then
+
+ elpi_CI_REF=proof+recthms
+ elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+ equations_CI_REF=proof+recthms
+ equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+ mtac2_CI_REF=proof+recthms
+ mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+ paramcoq_CI_REF=proof+recthms
+ paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+ quickchick_CI_REF=proof+recthms
+ quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi