From e6533c9152bb489b4804f5cdbe0c4d57893d3854 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Tue, 24 Jun 2025 17:58:53 +0100
Subject: Fix 38--41.

---
 sec/intro.ltx | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'sec/intro.ltx')

diff --git a/sec/intro.ltx b/sec/intro.ltx
index e60410a..26b3a7d 100644
--- a/sec/intro.ltx
+++ b/sec/intro.ltx
@@ -52,7 +52,9 @@ Developing these non-trivial recursive programs requires good tools
 for using \lang{}. To that end, we have implemented a certifying type
 checker and a compiler into Scheme. Our type checker not only checks
 whether a \lang{} program is well/ill-typed, but it also provides a
-proof for its decision.
+proof for its decision. The compiler needs this certificate when
+compiling \lang{} into Scheme, so that it has enough type information
+to compile \foldkw{}.
 
 \subsubsection*{Contributions}%
 In this paper we:
-- 
cgit v1.2.3