diff options
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 6 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 13 |
2 files changed, 17 insertions, 2 deletions
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 1f7fbcbf6..bfa43cde1 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 0b0c0f5bf..7fad65bf0 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. |