diff options
| author | coqbot-app[bot] | 2020-11-16 17:14:37 +0000 |
|---|---|---|
| committer | GitHub | 2020-11-16 17:14:37 +0000 |
| commit | 04b25a7635e796ad05ef7db537883594a5144a56 (patch) | |
| tree | 75e0efa3f2e1b924dbe54dc1736fd9f28346b7c1 /dev | |
| parent | 29dc0d5b8951bb467bb2cc473a90e8feaadbb9b8 (diff) | |
| parent | 6f31beeaaaf99306d206964e1bd3e966b0475023 (diff) | |
Merge PR #12873: Unification: A type-checking fix in imitation + an error locating fix
Reviewed-by: gares
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh b/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh new file mode 100644 index 0000000000..7680e8da78 --- /dev/null +++ b/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh @@ -0,0 +1,6 @@ +if [ "$CI_PULL_REQUEST" = "12873" ] || [ "$CI_BRANCH" = "master+minifix-unification-error-reporting-recheck-applications" ]; then + + equations_CI_REF=master+fix12873-better-unification + equations_CI_GITURL=https://github.com/herbelin/Coq-Equations + +fi |