From 44ca9c2d6a6f1eef5ba5319472ce75567a4821f2 Mon Sep 17 00:00:00 2001
From: BlackBrane <cs.hbar@gmail.com>
Date: Sun, 2 Aug 2015 19:49:43 +0200
Subject: [PATCH 1/2] Remove spurious Data.Fin imports (now reexported by Vect)

---
 libs/base/Data/HVect.idr       | 1 -
 libs/effects/Effect/Random.idr | 1 -
 2 files changed, 2 deletions(-)

diff --git a/libs/base/Data/HVect.idr b/libs/base/Data/HVect.idr
index b6e8badd28..acccb9c65a 100644
--- a/libs/base/Data/HVect.idr
+++ b/libs/base/Data/HVect.idr
@@ -1,6 +1,5 @@
 module Data.HVect
 
-import Data.Fin
 import public Data.Vect
 
 %access public
diff --git a/libs/effects/Effect/Random.idr b/libs/effects/Effect/Random.idr
index b10c91f727..55a08fc1d7 100644
--- a/libs/effects/Effect/Random.idr
+++ b/libs/effects/Effect/Random.idr
@@ -2,7 +2,6 @@ module Effect.Random
 
 import Effects
 import Data.Vect
-import Data.Fin
 
 data Random : Effect where 
      getRandom : sig Random Integer Integer

From afe94818717c8b6d81a08e8dbc759e2009a6f67e Mon Sep 17 00:00:00 2001
From: BlackBrane <cs.hbar@gmail.com>
Date: Mon, 3 Aug 2015 14:02:34 +0200
Subject: [PATCH 2/2] Make clear that sum' is a synonym for concat

---
 libs/contrib/Control/Algebra.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/libs/contrib/Control/Algebra.idr b/libs/contrib/Control/Algebra.idr
index afde92318e..23335ee02b 100644
--- a/libs/contrib/Control/Algebra.idr
+++ b/libs/contrib/Control/Algebra.idr
@@ -116,7 +116,7 @@ class RingWithUnity a => Field a where
   inverseM : (x : a) -> Not (x = neutral) -> a
 
 sum' : (Foldable t, Monoid a) => t a -> a
-sum' = foldr (<+>) neutral
+sum' = concat
 
 product' : (Foldable t, RingWithUnity a) => t a -> a
 product' = foldr (<.>) unity