Mercurial > cpdt > repo
comparison src/Universes.v @ 510:fd6ec9b2dccb
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 |
comparison
equal
deleted
inserted
replaced
| 509:21079e42b773 | 510:fd6ec9b2dccb |
|---|---|
| 369 Error: Impossible to unify "?35 = ?34" with "unit = unit". | 369 Error: Impossible to unify "?35 = ?34" with "unit = unit". |
| 370 >> | 370 >> |
| 371 | 371 |
| 372 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! | 372 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! |
| 373 | 373 |
| 374 The following command is the secret to getting better error messages in such cases: *) | 374 The following command is the secret to getting better error messages in such cases:%\index{Vernacular commands!Set Printing All}% *) |
| 375 | 375 |
| 376 Set Printing All. | 376 Set Printing All. |
| 377 (** %\vspace{-.15in}%[[ | 377 (** %\vspace{-.15in}%[[ |
| 378 apply symmetry. | 378 apply symmetry. |
| 379 ]] | 379 ]] |