### diff src/Universes.v @ 510:fd6ec9b2dccb

Finished last pass through the book before beginning the MIT Press editorial process
author Adam Chlipala Wed, 13 Feb 2013 10:22:18 -0500 2036ef0bc891 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}%[[