[Changed the type of run-cong.
Nils Anders Danielsson <nils.anders.danielsson@gmail.com>**20101211170246
 Ignore-this: e3ef1247bf09fa0c2bc532c9890f0f8a
] hunk ./CompositionBased.agda 173
+  open P.≡-Reasoning
hunk ./CompositionBased.agda 188
-      where open P.≡-Reasoning
hunk ./CompositionBased.agda 191
-      where open P.≡-Reasoning
hunk ./CompositionBased.agda 192
-      where open P.≡-Reasoning
hunk ./CompositionBased.agda 194
-  correct e = H.≅-to-≡ (begin
+  correct e = begin
hunk ./CompositionBased.agda 196
-    run ⟦ e ⟧↑                                            ≅⟨ run-cong (Defunctionalised.correct e) ⟩
+    run ⟦ e ⟧↑                                            ≡⟨ run-cong (Defunctionalised.correct e) ⟩
hunk ./CompositionBased.agda 199
-    exec (comp e halt) []                                 ∎)
-    where open H.≅-Reasoning
+    exec (comp e halt) []                                 ∎
hunk ./CompositionBased/Exceptions.agda 302
+  open P.≡-Reasoning
hunk ./CompositionBased/Exceptions.agda 318
-      where open P.≡-Reasoning
hunk ./CompositionBased/Exceptions.agda 322
-      where open P.≡-Reasoning
hunk ./CompositionBased/Exceptions.agda 326
-      where open P.≡-Reasoning
hunk ./CompositionBased/Exceptions.agda 328
-      where open P.≡-Reasoning
hunk ./CompositionBased/Exceptions.agda 330
-      where open P.≡-Reasoning
hunk ./CompositionBased/Exceptions.agda 332
-  correct e = H.≅-to-≡ (begin
+  correct e = begin
hunk ./CompositionBased/Exceptions.agda 334
-    run ⟦ e ⟧↑                                                  ≅⟨ run-cong (Defunctionalised.correct e) ⟩
+    run ⟦ e ⟧↑                                                  ≡⟨ run-cong (Defunctionalised.correct e) ⟩
hunk ./CompositionBased/Exceptions.agda 337
-    exec (comp e halt crash) []                                 ∎)
-    where open H.≅-Reasoning
+    exec (comp e halt crash) []                                 ∎
hunk ./ReverseComposition.agda 145
-run-cong : ∀ {ℓ} {B₁ B₂ : Set ℓ} {x₁ : [] ⇨ B₁} {x₂ : [] ⇨ B₂} →
-           x₁ ≈ x₂ → run x₁ ≅ run x₂
-run-cong (return-cong x₁≡x₂) = H.≡-to-≅ x₁≡x₂
+run-cong : ∀ {ℓ} {B : Set ℓ} {x₁ x₂ : [] ⇨ B} →
+           x₁ ≈ x₂ → run x₁ ≡ run x₂
+run-cong (return-cong x₁≡x₂) = x₁≡x₂