[Replaced the syntax Σ[ x ∶ A ] B with Σ[ x ∈ A ] B.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20120506171416
 Ignore-this: de9703959a0f42cf81466c21c4a22a9
] hunk ./src/Data/AVL/IndexedMap.agda 37
-  fromKV : KV → Σ[ ik ∶ ∃ Key ] Value (proj₁ ik)
+  fromKV : KV → Σ[ ik ∈ ∃ Key ] Value (proj₁ ik)
hunk ./src/Data/AVL/IndexedMap.agda 40
-  toKV : Σ[ ik ∶ ∃ Key ] Value (proj₁ ik) → KV
+  toKV : Σ[ ik ∈ ∃ Key ] Value (proj₁ ik) → KV
hunk ./src/Data/Container.agda 40
-⟦ C ⟧ X = Σ[ s ∶ Shape C ] (Position C s → X)
+⟦ C ⟧ X = Σ[ s ∈ Shape C ] (Position C s → X)
hunk ./src/Data/Container.agda 47
-  Σ[ eq ∶ s ≡ s′ ] (∀ p → f p ≈ f′ (P.subst (Position C) eq p))
+  Σ[ eq ∈ s ≡ s′ ] (∀ p → f p ≈ f′ (P.subst (Position C) eq p))
hunk ./src/Data/Product.agda 28
-syntax Σ A (λ x → B) = Σ[ x ∶ A ] B
+syntax Σ A (λ x → B) = Σ[ x ∈ A ] B
hunk ./src/Data/Product.agda 41
-A × B = Σ[ x ∶ A ] B
+A × B = Σ[ x ∈ A ] B
hunk ./src/Relation/Nullary/Negation.agda 141
-    Q → (P → Σ Q R) → ¬ ¬ (Σ[ x ∶ Q ] (P → R x))
+    Q → (P → Σ Q R) → ¬ ¬ (Σ[ x ∈ Q ] (P → R x))