diff options
| author | Hugo Herbelin | 2020-04-05 14:13:54 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-04-21 19:33:19 +0200 |
| commit | c6815a6cd004a1ab4852414127fef6f8f77894bb (patch) | |
| tree | 35e27c74f403844f4fa0408c42109ab20c94cfad /dev | |
| parent | dcced70a3ac146efb2f6214e197ef4b0d73debb1 (diff) | |
Adding a Declare ML Module in empty file Ltac.v.
Indeed, it would be intuitive that `Require Import Ltac` is an
equivalent for Ltac of `Require Import Ltac2.Ltac2`.
Also declaring the classic proof mode.
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..e2c27c939e --- /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+fix12023-atomic-tactic-now-qualified-in-ltac-file + fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto + + mtac2_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file + mtac2_CI_GITURL=https://github.com/herbelin/Mtac2 + + metacoq_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file + metacoq_CI_GITURL=https://github.com/herbelin/template-coq + + unimath_CI_REF=master+fix12023-atomic-tactic-now-qualified-in-ltac-file + unimath_CI_GITURL=https://github.com/herbelin/UniMath + +fi |