[Made the code build using recent versions of its dependencies.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20161208102317
 Ignore-this: 9c1daa1f0d62e146197fb1724ac7c55e
] hunk ./CompositionBased/Exceptions.agda 14
+import Level
hunk ./CompositionBased/Exceptions.agda 19
-  open module M = RawMonadPlus Maybe.monadPlus
+  open module M = RawMonadPlus (Maybe.monadPlus {f = Level.zero})
hunk ./CompositionBased/Lambda.agda 5
-open import Level
+import Level
hunk ./CompositionBased/Lambda.agda 12
-         (ext : P.Extensionality zero zero) where
+         (ext : P.Extensionality Level.zero Level.zero) where
hunk ./CompositionBased/Lambda.agda 17
-open import Function
+open import Function hiding (_∋_)
hunk ./CompositionBased/Lambda.agda 56
-  Σ[ x ∶ ⟦ σ ⟧ ] Ctxt-interpretation ⟦_⟧ Γ
+  Σ[ x ∈ ⟦ σ ⟧ ] Ctxt-interpretation ⟦_⟧ Γ
hunk ./CompositionBased/Lambda.agda 134
-  infix  2 _∎
+  infix  3 _∎
hunk ./DanvyFirstAttempt.agda 15
-open import Function
+open import Function hiding (_∋_)
hunk ./Exceptions.agda 29
+import Level
hunk ./Exceptions.agda 32
-open RawMonadPlus Maybe.monadPlus
+open RawMonadPlus (Maybe.monadPlus {f = Level.zero})
hunk ./FailureAndNonDeterminism.agda 15
+import Level
hunk ./FailureAndNonDeterminism.agda 20
-  module LM = RawMonadPlus List.monadPlus
+  module LM = RawMonadPlus (List.monadPlus {ℓ = Level.zero})
hunk ./FailureAndNonDeterminism.agda 36
-open RawMonad (Maybe.monadT List.monad) public
+open RawMonad (Maybe.monadT (List.monad {ℓ = Level.zero})) public
hunk ./ReverseComposition.agda 12
-open import Data.Maybe as Maybe
+open import Data.Maybe as Maybe hiding (map)
hunk ./ReverseComposition.agda 18
-open import Level
+open import Level using (Lift; lift)
hunk ./ReverseComposition.agda 65
-               As₁ ⇨ B₁ → As₂ ⇨ B₂ → Set (suc ℓ) where
+               As₁ ⇨ B₁ → As₂ ⇨ B₂ → Set (Level.suc ℓ) where
hunk ./ReverseComposition.agda 98
-  infix  2 _∎
+  infix  3 _∎
hunk ./ReverseComposition.agda 123
-  EqualTo : ∀ {ℓ As} {B : Set ℓ} → As ⇨ B → Set (suc ℓ)
+  EqualTo : ∀ {ℓ As} {B : Set ℓ} → As ⇨ B → Set (Level.suc ℓ)
hunk ./ReverseComposition.agda 819
-infixl 5 _⇨M_
+infixl 4 _⇨M_
hunk ./Wand2.agda 23
-open import Function
+open import Function hiding (_∋_)
hunk ./Wand2.agda 68
-  args = ε {NonEmpty _} ▻ ↦ x ▻ ↦ y
+  args = ε {I = NonEmpty _} ▻ ↦ x ▻ ↦ y