From a5f64d1721927c16a7536b39ce0bac419dda28f1 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 14 Dec 2018 08:08:24 +0100
Subject: [PATCH] Fix typo in Changelog.

---
 CHANGELOG.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 83b1c8615..f7b0037ea 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -63,7 +63,7 @@ Changes in Coq:
   - Big-ops are automatically imported, imports of `iris.base_logic.big_op` have
     to be removed.
   - The âŠ¢ notation can sometimes infer different (but convertible) terms when
-    seraching for the BI to use, which (due to Coq limitations) can lead to
+    searching for the BI to use, which (due to Coq limitations) can lead to
     failing rewrites, in particular when rewriting at function types.
 * The `iInv` tactic can now be used without the second argument (the name for
   the closing update).  It will then instead add the obligation to close the
-- 
GitLab