diff options
| author | Emilio Jesus Gallego Arias | 2020-04-22 18:37:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-04-22 18:37:11 +0200 |
| commit | 3c0ba7afdf289bc1c50f3458d6c5da685f0b160c (patch) | |
| tree | 892789e78c3c3dd3226d63398ded312d7ccf47b1 /dev | |
| parent | 0c4775fcb48207c96752b81c76f67c17e5fd3c99 (diff) | |
| parent | 9664a490ac3755b19ed9b8ec6a2f1925d9ec79ac (diff) | |
Merge PR #12023: Adding a Declare ML Module in empty file Ltac.v
Ack-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: ppedrot
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh | 15 |
1 files changed, 15 insertions, 0 deletions
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 |