From c9919add0fe4cc64021aa0fe676527199fccd245 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 26 Jun 2025 18:16:14 +0100
Subject: Fix 925--927.

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

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index 3a3cebc..efe7cf2 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -17,7 +17,8 @@ three main components:
 
   \item Second we perform type checking using a bidirectional
     algorithm~\cite{bidir}. Along with the usual type checking result,
-    the algorithm produces a runtime-erased typing derivation.
+    the algorithm produces a runtime-erased certificate that a term is
+    well/ill typed.
 
   \item Finally we compile the term to Guile~Scheme~\cite{guile}. By
     requiring an erased type derivation, the compiler can statically
-- 
cgit v1.2.3