aboutsummaryrefslogtreecommitdiff
path: root/dev
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-03-06 20:58:26 +0100
committerGaëtan Gilbert2019-03-06 20:58:26 +0100
commitc9fd99644e223ada3aad53915f1cd0d2598882b3 (patch)
tree784938d42cf4c37436c305cf625d240c154ac9c9 /dev
parenta83eac8463787c13a2dbd3903baf2b59ca1a4635 (diff)
parent7b724139a09c5d875131c5861a32d225d5b4b07b (diff)
Merge PR #9476: Constructor type information uses the expanded form.
Reviewed-by: SkySkimmer Reviewed-by: gares
Diffstat (limited to 'dev')
-rw-r--r--dev/ci/user-overlays/09476-ppedrot-context-constructor.sh9
1 files changed, 9 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh
new file mode 100644
index 0000000000..1af8b5430d
--- /dev/null
+++ b/dev/ci/user-overlays/09476-ppedrot-context-constructor.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "9476" ] || [ "$CI_BRANCH" = "context-constructor" ]; then
+
+ quickchick_CI_REF=context-constructor
+ quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
+
+ equations_CI_REF=context-constructor
+ equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi