# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1346275037 14400
# Node ID e53d051681b031145096fa0c23047170f722d77b
# Parent  218361342cd2bc216f2a3c5b989e056b533a3a3a
Finish complete proofreading pass

diff -r 218361342cd2 -r e53d051681b0 latex/cpdt.bib
--- a/latex/cpdt.bib	Wed Aug 29 17:03:19 2012 -0400
+++ b/latex/cpdt.bib	Wed Aug 29 17:17:17 2012 -0400
@@ -17,7 +17,7 @@
   title = {A Mechanically Checked Proof of the Correctness of the Kernel of the {AMD5k86} Floating-Point Division Algorithm},
   journal = {IEEE Transactions on Computers},
   volume = {47(9)},
-  pages = {913--926}
+  pages = {913--926},
   year = {1998}
 }
 
@@ -162,7 +162,7 @@
  title = {Higher-order abstract syntax},
  booktitle = {Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation},
  year = {1988},
- pages = {199--208},
+% pages = {199--208},
 } 
 
 @article{HOU,
@@ -300,7 +300,7 @@
  title = {How to make ad-hoc polymorphism less ad hoc},
  booktitle = {Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
  year = {1989},
- pages = {60--76},
+% pages = {60--76},
 } 
 
 @inproceedings{reflection,
diff -r 218361342cd2 -r e53d051681b0 src/ProgLang.v
--- a/src/ProgLang.v	Wed Aug 29 17:03:19 2012 -0400
+++ b/src/ProgLang.v	Wed Aug 29 17:17:17 2012 -0400
@@ -330,7 +330,7 @@
   | Let : forall t1 t2, term t1 -> (term t1 -> term t2) -> term t2.
 ]]
 
-   However, Coq rejects this definition for failing to meet the %\index{strict positivity restriction}%strict positivity restriction.  For instance, the constructor [Abs] takes an argument that is a function over the same type family [term] that we are defining.  Inductive definitions of this kind can be used to write non-terminating Gallina programs, which breaks the consistency of Coq's logic.
+   However, Coq rejects this definition for failing to meet the %\index{strict positivity requirement}%strict positivity restriction.  For instance, the constructor [Abs] takes an argument that is a function over the same type family [term] that we are defining.  Inductive definitions of this kind can be used to write non-terminating Gallina programs, which breaks the consistency of Coq's logic.
 
    An alternate higher-order encoding is%\index{parametric higher-order abstract syntax}\index{PHOAS}% _parametric HOAS_, as introduced by Washburn and Weirich%~\cite{BGB}% for Haskell and tweaked by me%~\cite{PhoasICFP08}% for use in Coq.  Here the idea is to parametrize the syntax type by a type family standing for a _representation of variables_. *)