Merge master into experimental following 1.5 release (#1431)

Author: gallais

.travis.yml

@@ -155,10 +155,10 @@ matrix:
         - git remote add upstream https://[email protected]/agda/agda-stdlib.git &>/dev/null
         - git fetch upstream && git reset upstream/gh-pages
         - if [[ $TRAVIS_BRANCH = "master" ]]; then
-            git checkout HEAD -- v0.16/ v0.17/ v1.0/ v1.1/ v1.2/ v1.3/ v1.4/ experimental/ ;
+            git checkout HEAD -- v0.16/ v0.17/ v1.0/ v1.1/ v1.2/ v1.3/ v1.4/ v1.5/ experimental/ ;
           fi
         - if [[ $TRAVIS_BRANCH = "experimental" ]]; then
-            git checkout HEAD -- *.html v0.16/ v0.17/ v1.0/ v1.1/ v1.2/ v1.3/ v1.4/ ;
+            git checkout HEAD -- *.html v0.16/ v0.17/ v1.0/ v1.1/ v1.2/ v1.3/ v1.4/ v1.5/ ;
           fi
         - git add -f \*.html
         - git commit -m "Automatic HTML update via Travis"