# HG changeset patch # User Adam Chlipala # Date 1334270815 14400 # Node ID fd3f1057685c322c58ed3ec78b3070cea4feac7d # Parent fc499b720a0a2a5a9bbca033c38100bd47a3f998 Typo fix diff -r fc499b720a0a -r fd3f1057685c staging/updates.rss --- a/staging/updates.rss Thu Apr 12 18:45:48 2012 -0400 +++ b/staging/updates.rss Thu Apr 12 18:46:55 2012 -0400 @@ -16,7 +16,7 @@ Thu, 12 Apr 2012 18:42:46 EDT http://adam.chlipala.net/cpdt/ adamc@csail.mit.edu - Stronger theorem at end of "Infinite Data and Proofs" chapter; in "Reasoning About Equality Proofs" chapter, more discussion of axiom avoidance and tactic pitfalls for JMeq; general passes through "Proof Ssearch in Ltac" and "Proving in the Large" chapters; in "Universes and Axioms" chapter, a class of baffling error messages explained; comments added to CpdtTactics.v. + Stronger theorem at end of "Infinite Data and Proofs" chapter; in "Reasoning About Equality Proofs" chapter, more discussion of axiom avoidance and tactic pitfalls for JMeq; general passes through "Proof Search in Ltac" and "Proving in the Large" chapters; in "Universes and Axioms" chapter, a class of baffling error messages explained; comments added to CpdtTactics.v.