Mercurial > cpdt > repo

diff src/Subset.v @ 294:1b6c81e51799

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Fixes added while proofreading JFR camera-ready
author Adam Chlipala <adam@chlipala.net>
date Thu, 09 Dec 2010 13:44:57 -0500
parents 2c88fc1dbe33
children b441010125d4
line wrap: on
line diff
--- a/src/Subset.v	Wed Nov 10 16:34:46 2010 -0500
+++ b/src/Subset.v	Thu Dec 09 13:44:57 2010 -0500
@@ -84,7 +84,7 @@
  
  ]]
 
- One aspect in particular of the definition of [pred_strong1] may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.
+One aspect in particular of the definition of [pred_strong1] may be surprising.  We took advantage of [Definition]'s syntactic sugar for defining function arguments in the case of [n], but we bound the proofs later with explicit [fun] expressions.  Let us see what happens if we write this function in the way that at first seems most natural.
 
 [[
 Definition pred_strong1' (n : nat) (pf : n > 0) : nat :=