Fix 967--979.

1 files changed, 5 insertions, 13 deletions

diff --git a/sec/compiler.ltx b/sec/compiler.ltx
index 27705b6..f1abca9 100644
--- a/sec/compiler.ltx
+++ b/sec/compiler.ltx
@@ -78,22 +78,14 @@ before the third combinator and so on.
 The parser returns an intrinsically well-scoped
 term~\cite{iwss}. Terms are a dependent data type with signature
 \verb|Context -> Type|. All variable names within a term are
-guaranteed to be bound within the context parameter or a term
+guaranteed to be bound within the context parameter or by a term
 constructor such as \letkw{} or \foldkw{}. The term is
 \emph{intrinsically} well-scoped because the binding rules are
 enforced by the term constructors; an extrinsically well-scoped term
-would use a separate predicate to prove raw syntax is well-scoped.
-
-Normally parsers produce ``raw'' abstract syntax trees with concrete
-names instead of deBruijn indices. We use dependant state to directly
-create the well-scoped AST because starting from a well-scoped AST
-simplifies the type checker.
-
-We also had the option to produce a raw AST and an extrinsic
-certificate it is well-scoped. Extrinsic certificates are best for
-certifying properties of preexisting structures. As our parser is
-creating the well-scoped AST, the raw AST cannot have been used in any
-prior computations, so we do not need to reference the raw AST.
+would use a separate predicate to prove raw syntax is well-scoped.  As
+our parser is creating the well-scoped AST, the raw AST cannot have
+been used in any prior computations, so we do not need to reference a
+raw AST.\@
 
 \subsection{Bidirectional Type Checker}