Merge branch 'master' into experimental

Author: MatthewDaggitt

.travis.yml

@@ -57,11 +57,11 @@ install:
     cp -a $HOME/.ghc $HOME/.cabsnap/ghc;
     cp -a $HOME/.cabal/lib $HOME/.cabal/share $HOME/.cabal/bin $HOME/installplan.txt $HOME/.cabsnap/;
   # installing fix-agda-whitespace
-  - cd src/fix-agda-whitespace
-  - cabal install fix-agda-whitespace.cabal
-  - cd ../../..
-  - yes | rm -R agda/
-  - cd agda-stdlib
+  - git clone https://github.com/agda/fix-whitespace --depth=1
+  - cd fix-whitespace
+  - cabal install fix-whitespace.cabal
+  - cd -
+  - yes | rm -R fix-whitespace/
   # generating Everything.agda
   - cabal install lib.cabal
   - runghc GenerateEverything.hs
@@ -75,7 +75,7 @@ script:
   # generating index.agda
   - ./index.sh
   # detecting whitespace violations
-  - make check-whitespace
+  - fix-whitespace --check
   # expose the value of RTS_OPTIONS
   - echo $RTS_OPTIONS
   # checking safe modules build with --safe

CHANGELOG.md

@@ -42,6 +42,9 @@ Bug-fixes
   `_<′_` as do all the old proofs, e.g. `+-monoˡ-<` has become `+-monoˡ-<′`,
   but these have all been deprecated and may be removed in some future version.
 
+* Migrating code might require lemmas relating `m < n` and `m <′ n`/`suc m ≤ n`;
+  such lemmas have unfortunately only been added in 1.3.
+
 #### Fixed wrong queries being exported by `Data.Rational`
 
 * `Data.Rational` previously accidently exported queries from `Data.Nat.Base`