diff options
| author | Maxime Dénès | 2017-05-25 12:49:12 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-25 12:49:12 +0200 |
| commit | 2f75922ad52e334b7bcc3a26c2ecb1602c85fc2f (patch) | |
| tree | 3ba950c021df581a004a4af158880558eb2dbe14 /dev | |
| parent | 03e4f9c3da333d13553b4ea3247b0c36c124995e (diff) | |
| parent | cb316573aa1d09433531e7c67e320c14ef05c3e2 (diff) | |
Merge PR#481: [option] Remove support for non-synchronous options.
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/ci/ci-user-overlay.sh | 20 | ||||
| -rw-r--r-- | dev/doc/changes.txt | 7 |
2 files changed, 9 insertions, 18 deletions
diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh index 71d098e378..1f7fbcbf68 100644 --- a/dev/ci/ci-user-overlay.sh +++ b/dev/ci/ci-user-overlay.sh @@ -25,24 +25,8 @@ echo $TRAVIS_PULL_REQUEST echo $TRAVIS_BRANCH echo $TRAVIS_COMMIT -if [ $TRAVIS_PULL_REQUEST == "402" ] || [ $TRAVIS_BRANCH == "located_switch" ]; then - - mathcomp_CI_BRANCH=located_switch +if [ $TRAVIS_PULL_REQUEST == "481" ] || [ $TRAVIS_BRANCH == "options+remove_non_sync" ]; then + mathcomp_CI_BRANCH=options+remove_non_sync mathcomp_CI_GITURL=https://github.com/ejgallego/math-comp.git - - fiat_parsers_CI_BRANCH=located_switch - fiat_parsers_CI_GITURL=https://github.com/ejgallego/fiat.git - - bedrock_src_CI_BRANCH=located_switch - bedrock_src_CI_GITURL=https://github.com/ejgallego/bedrock.git - - bedrock_facade_CI_BRANCH=located_switch - bedrock_facade_CI_GITURL=https://github.com/ejgallego/bedrock.git - -fi - -if [ $TRAVIS_PULL_REQUEST == "406" ] || [ $TRAVIS_BRANCH == "feature/coq_makefile2" ]; then - UniMath_CI_BRANCH=master - UniMath_CI_GITURL=https://github.com/gares/UniMath.git fi diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 527721f8a4..a2ae8254db 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -101,6 +101,13 @@ type 'a ast = private { implemented in the whole code base. Matching a located object hasn't changed, however, `Loc.tag ?loc obj` must be used to build one. +In GOption: + + Support for non-synchronous options has been removed. Now all + options are handled as a piece of normal document state, and thus + passed to workers, etc... As a consequence, the field + `Goptions.optsync` has been removed. + ** Tactic API ** - pf_constr_of_global now returns a tactic instead of taking a continuation. |