From be0d6912ad1cfe9e63c47d5d52d8b00ec97ea4c3 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Franc=CC=A7ois=20Pottier?= <francois.pottier@inria.fr>
Date: Mon, 11 Nov 2024 14:08:17 +0100
Subject: [PATCH] README.

---
 README.md | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/README.md b/README.md
index 3d1e70c..1335d6f 100644
--- a/README.md
+++ b/README.md
@@ -84,15 +84,13 @@ The syllabus is organized in four main segments of five lectures each.
   * (Same slides).
 
 * (12/11/2024) The CPS transformation (FP).
-
-  * ([slides 06](slides/fpottier-06.pdf),
+  + ([slides 06](slides/fpottier-06.pdf),
      [slides without animations 06](slides/fpottier-printing-06.pdf)).
 
   A proof of type soundness in Coq (FP).
-
-  * [definition of simply-typed λ-calculus](coq/STLCDefinition.v)
-  * [auxiliary lemmas and judgements](coq/STLCLemmas.v)
-  * subject reduction and progress: [template](coq/STLCTypeSoundnessBlank.v), [solution](coq/STLCTypeSoundnessComplete.v)
+  + [definition of simply-typed λ-calculus](coq/STLCDefinition.v)
+  + [auxiliary lemmas and judgements](coq/STLCLemmas.v)
+  + subject reduction and progress: [template](coq/STLCTypeSoundnessBlank.v), [solution](coq/STLCTypeSoundnessComplete.v)
 
 * (19/11/2024) Semantic type soundness for System F with mutable state in Coq/Iris (JHJ).
   * ([slides](slides/jhjourdan-00.pdf), [Coq/Iris development](coq/logic_rel.tar.gz))
-- 
GitLab