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 ]]