diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-common.sh | 13 | ||||
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 6 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 15 |
3 files changed, 28 insertions, 6 deletions
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh index 2711b7ecaa..f1e1515d41 100644 --- a/dev/ci/ci-common.sh +++ b/dev/ci/ci-common.sh @@ -2,11 +2,18 @@ set -xe +if [ -n "${GITLAB_CI}" ]; +then + export COQBIN=`pwd`/install/bin +else + export COQBIN=`pwd`/bin +fi +export PATH="$COQBIN:$PATH" + # Coq's tools need an ending slash :S, we should fix them. -export COQBIN=`pwd`/bin/ -export PATH=`pwd`/bin:$PATH +export COQBIN="$COQBIN/" -ls `pwd`/bin +ls "$COQBIN" # Where we clone and build external developments CI_BUILD_DIR=`pwd`/_build_ci diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 1f7fbcbf68..bfa43cde1d 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -25,8 +25,10 @@ echo $TRAVIS_PULL_REQUEST echo $TRAVIS_BRANCH echo $TRAVIS_COMMIT -if [ $TRAVIS_PULL_REQUEST == "481" ] || [ $TRAVIS_BRANCH == "options+remove_non_sync" ]; then - mathcomp_CI_BRANCH=options+remove_non_sync +if [ $TRAVIS_PULL_REQUEST == "678" ] || [ $TRAVIS_BRANCH == "coqlib-part-02" ]; then + + mathcomp_CI_BRANCH=coqlib-part-02 mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git + fi diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index d52c184623..7fad65bf0a 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -108,6 +108,19 @@ In GOption: passed to workers, etc... As a consequence, the field `Goptions.optsync` has been removed. +In Coqlib / reference location: + + We have removed from Coqlib functions returning `constr` from + names. Now it is only possible to obtain references, that must be + processed wrt the particular needs of the client. + + Users of `coq_constant/gen_constant` can do + `Universes.constr_of_global (find_reference dir r)` _however_ note + the warnings in the `Universes.constr_of_global` in the + documentation. It is very likely that you were previously suffering + from problems with polymorphic universes due to using + `Coqlib.coq_constant` that used to do this. + ** Tactic API ** - pf_constr_of_global now returns a tactic instead of taking a continuation. @@ -162,7 +175,7 @@ uses type classes and rejects terms with unresolved holes. functions that used to carry a suffix `_loc`, such suffix has been dropped. -- `errorlabstrm` has been removed in favor of `user_err`. +- `errorlabstrm` and `error` has been removed in favor of `user_err`. - The header parameter to `user_err` has been made optional. |