Mercurial > cpdt > repo

diff src/Universes.v @ 510:fd6ec9b2dccb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finished last pass through the book before beginning the MIT Press editorial process
author Adam Chlipala <adam@chlipala.net>
date Wed, 13 Feb 2013 10:22:18 -0500
parents 2036ef0bc891
children ed829eaa91b2
line wrap: on
line diff
--- a/src/Universes.v	Tue Feb 12 11:14:52 2013 -0500
+++ b/src/Universes.v	Wed Feb 13 10:22:18 2013 -0500
@@ -371,7 +371,7 @@
 
 Coq tells us that we cannot, in fact, apply our lemma [symmetry] here, but the error message seems defective.  In particular, one might think that [apply] should unify [?35] and [?34] with [unit] to ensure that the unification goes through.  In fact, the issue is in a part of the unification problem that is _not_ shown to us in this error message!
 
-The following command is the secret to getting better error messages in such cases: *)
+The following command is the secret to getting better error messages in such cases:%\index{Vernacular commands!Set Printing All}% *)
 
   Set Printing All.
   (** %\vspace{-.15in}%[[