From cab152fd3aea9e3eddf8432b16643d01bf908ba1 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Sun, 13 May 2018 15:32:30 +0200
Subject: Minor textual enhancements

---
 expr.tex | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/expr.tex b/expr.tex
index df2800a..ddaf3a1 100644
--- a/expr.tex
+++ b/expr.tex
@@ -28,9 +28,8 @@ The \textsf{Exp} compiler, its semantics, the compiler and the proof
 The Coq file is attached to this report.
 The report walks through the file, but occasionally discusses things out of order when this aids understandability.
 
-The proof uses well-founded induction, which requires a library.
-We also use the \textsf{Omega} library for basic arithmetic,
-	and the \textsf{ListNotations} module for pretty list notation.
+The proof uses well-founded induction, which is most easily done with the \textsf{Wellfounded} library.
+We also use \textsf{Omega} for basic arithmetic and the \textsf{ListNotations} module for pretty list notation.
 
 \coq{1}{2}
 
@@ -125,7 +124,6 @@ Since the program is reversed for use in \textsf{pn\_eval}, we can rewrite the p
 
 \coq{76}{78}
 
-We now consider the rest of the program.
 Suppose the original expression was \textsf{e = eadd e1 e2},
 	we now consider \textsf{pn\_eval v env ((rev (rpn v e1) ++ rev (rpn v e2)) ++ rest)}
 	in the evaluation of \textsf{rpnadd}.
-- 
cgit v1.2.3