Fix 941--947.

1 files changed, 4 insertions, 4 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index f7a53b3..e8c1664 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -38,10 +38,10 @@ staged compiler for expressions using MetaML~\cite{metaml}. The
 interpreter only reports errors about the combinators at run time.
 
 We adapted the combinator interpreter for Idris 2. First, we used
-dependant types to statically enforce a combinator is well-formed. The
-``parse'' interpretation function requires a certificate that a parser
-is well-formed. Second, our interpreter produces a certificate that
-the list of unprocessed tokens is a suffix of the input tokens. This
+dependant types to statically enforce a combinator is well-formed; the
+interpretation function takes a certificate that a parser is
+well-formed. Second, our interpreter produces a certificate that the
+list of unprocessed tokens is a suffix of the input tokens. This
 certificate is required to satisfy the Idris termination checker when
 interpreting fixed point combinators. Finally, we thread state
 throughout the combinators.