...

diff --git a/presentation.tex b/presentation.tex
index a2cf6aba85c816091641715567119ec7903063ac..a8e4995d7a36b8314c159f2c5364d2e2ebe5721d 100644 (file)
--- a/presentation.tex
+++ b/presentation.tex
@@ -231,8 +231,8 @@
   \mykant\ is an \emph{interactive theorem prover}/\emph{functional
     programming language}, implemented in Haskell.
 
-  It is similar in scope to Agda or Coq, but with a more powerful notion
-  of \emph{equality}.
+  It is in the tradition of Agda and Epigram (and to a lesser extent
+  Coq), but with a more powerful notion of \emph{equality}.
 
   We have figured out theory of \mykant, and have a near-complete
   implementation.
@@ -374,7 +374,7 @@
   Or
   \[ \myfun{head} \myappsp (3 \mycons \mynil) : \myunit \myarr \mynat \]
 
-  Yes: to typecheck, we reduce terms fully (to their \emph{normal} form)
+  Yes: to typecheck, we reduce terms fully (to their \emph{normal form})
   before comparing:
   \[
   \begin{array}{@{}r@{\ }c@{\ }c@{\ }c@{\ }c@{\ }c@{\ }l}