From 7dc27a7bf10da12ac34b394ca23db8378bd82b00 Mon Sep 17 00:00:00 2001
From: dianne <diannes.gm@gmail.com>
Date: Sat, 19 Jan 2019 23:30:48 -0800
Subject: [PATCH] update agda-stdlib

this leaves us at commit d1e0ae9c9c9c7c99900d1806fbdb4c5082fc76fc
---
 Minesweeper/Board.agda       |  4 ++--
 Minesweeper/Enumeration.agda |  2 +-
 Minesweeper/Moves.agda       |  6 +++---
 Minesweeper/Reasoning.agda   | 10 +++++-----
 4 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/Minesweeper/Board.agda b/Minesweeper/Board.agda
index 75dcc31..c5a1d07 100644
--- a/Minesweeper/Board.agda
+++ b/Minesweeper/Board.agda
@@ -2,8 +2,8 @@ module Minesweeper.Board where
 
 open import Data.Vec as Vec using (Vec)
 import Data.Vec.Properties as VecProp
-import Data.Vec.Relation.Pointwise.Inductive   as VecIndPointwise
-import Data.Vec.Relation.Pointwise.Extensional as VecExtPointwise
+import Data.Vec.Relation.Binary.Pointwise.Inductive   as VecIndPointwise
+import Data.Vec.Relation.Binary.Pointwise.Extensional as VecExtPointwise
 open import Data.Fin using (_≟_)
 open import Data.Product
 open import Data.Product.Relation.Pointwise.NonDependent using (≡×≡⇒≡)
diff --git a/Minesweeper/Enumeration.agda b/Minesweeper/Enumeration.agda
index 516f6ed..7d9b5dc 100644
--- a/Minesweeper/Enumeration.agda
+++ b/Minesweeper/Enumeration.agda
@@ -3,7 +3,7 @@ module Minesweeper.Enumeration where
 open import Data.List as List using (List; []; _∷_)
 import Data.List.Categorical as List
 import Data.List.Properties as ListProp
-open import Data.List.Any as Any using (Any ; here ; there)
+open import Data.List.Relation.Unary.Any as Any using (Any ; here ; there)
 import Data.List.Any.Properties as AnyProp
 open import Data.List.Membership.Propositional
 import Data.List.Membership.Propositional.Properties as ∈Prop
diff --git a/Minesweeper/Moves.agda b/Minesweeper/Moves.agda
index bd93d82..c83ada3 100644
--- a/Minesweeper/Moves.agda
+++ b/Minesweeper/Moves.agda
@@ -6,9 +6,9 @@ open import Data.Empty
 open import Data.Product
 open import Data.Sum
 open import Data.Vec as Vec using (Vec; []; _∷_; _++_)
-open import Data.Vec.Relation.Pointwise.Inductive as VecPointwise using ([]; _∷_)
-open import Data.Vec.Any as Any using (Any; any)
-import      Data.Vec.Any.Properties as AnyProp
+open import Data.Vec.Relation.Unary.Any as Any using (Any; any)
+import      Data.Vec.Relation.Unary.Any.Properties as AnyProp
+open import Data.Vec.Relation.Binary.Pointwise.Inductive as VecPointwise using ([]; _∷_)
 open import Data.Vec.Membership.Propositional using (_∈_)
 import      Data.Vec.Membership.Propositional.Properties as ∈
 open import Data.Nat hiding (_>_; _≥_)
diff --git a/Minesweeper/Reasoning.agda b/Minesweeper/Reasoning.agda
index 3e37467..a9af769 100644
--- a/Minesweeper/Reasoning.agda
+++ b/Minesweeper/Reasoning.agda
@@ -7,12 +7,12 @@ open import Relation.Nullary
 open import Relation.Binary.PropositionalEquality
 open import Data.Empty
 open import Data.List as List using (List; []; _∷_)
-open import Data.List.Relation.Pointwise as Pointwise using (Pointwise; []; _∷_)
+open import Data.List.Relation.Unary.All as All using (All; []; _∷_)
+open import Data.List.Relation.Unary.All.Properties using (All¬⇒¬Any)
+open import Data.List.Relation.Unary.Any as Any using (Any; here; there)
+open import Data.List.Relation.Unary.Any.Properties using (there-injective)
+open import Data.List.Relation.Binary.Pointwise as Pointwise using (Pointwise; []; _∷_)
 open import Data.List.Membership.Propositional
-open import Data.List.All as All using (All; []; _∷_)
-open import Data.List.All.Properties using (All¬⇒¬Any)
-open import Data.List.Any as Any using (Any; here; there)
-open import Data.List.Any.Properties using (there-injective)
 open import Data.Product as Σ
 open import Data.Product.Properties
 open import Data.Nat