From e76f1db8aeab2ed4526a502d3c37697dee458764 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Sun, 16 Jul 2017 01:16:06 +0100
Subject: [PATCH] update README

---
 README.md            | 7 +++++--
 homotopy/serre.hlean | 1 -
 2 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index f57acd7..4dca86a 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,9 @@
 # Spectral Sequences
 
-Formalization project of the CMU HoTT group towards formalizing the Serre spectral sequence.
+Formalization project of the CMU HoTT group to formalize the Serre spectral sequence.
+
+*Update July 16*: The construction of the Serre spectral sequence has been completed. The result is `serre_convergence` in `homotopy.serre`.
+The main algebra part is in `algebra.spectral_sequence`.
 
 This repository also contains the contents of the MRC group on formalizing homology in Lean.
 
@@ -18,7 +21,7 @@ Jeremy Avigad, Steve Awodey, Ulrik Buchholtz, Floris van Doorn, Clive Newstead,
 
 ### Outline
 
-These projects are mostly done
+These projects are done
 
 - Given a sequence of spectra and maps, indexed over `ℤ`, we get an exact couple, indexed over `ℤ × ℤ`.
 - We can derive an exact couple.
diff --git a/homotopy/serre.hlean b/homotopy/serre.hlean
index 6fa77af..dfef176 100644
--- a/homotopy/serre.hlean
+++ b/homotopy/serre.hlean
@@ -267,5 +267,4 @@ section serre
  qed
 end serre
 
-
 end spectrum