changeset | ed829eaa91b2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Builds with Coq 8.5beta2 |
files |
changeset | fd6ec9b2dccb |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Finished last pass through the book before beginning the MIT Press editorial process |
files |
changeset | 2036ef0bc891 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through Chapter 12 |
files |
changeset | 31258618ef73 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Incorporate feedback from Nathan Collins |
files |
changeset | 40a9a36844d6 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Batch of changes based on proofreader feedback |
files |
changeset | 1fd4109f7b31 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Batch of changes based on proofreader feedback |
files |
changeset | b750ec0a8edb |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Proofreading pass through Chapter 12 |
files |
changeset | 0d66f1a710b8 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Vertical spacing through end of Part II |
files |
changeset | 8077352044b2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | A pass over all formatting, after big pile of coqdoc changes |
files |
changeset | 5d5e44f905c7 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Changes during more coqdoc hacking |
files |
changeset | a54a4a2ea6e4 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Changes while hacking on coqdoc |
files |
changeset | 5744842c36a8 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through Universes, to incorporate new coqdoc features |
files |
changeset | 5f25705a10ea |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl] |
files |
changeset | 686cf945dd02 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through StackMachine, to incorporate new coqdoc features |
files |
changeset | 539ed97750bb |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Update for Coq trunk version intended for final 8.4 release |
files |
changeset | 934945edc6b5 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Typesetting pass over Universes |
files |
changeset | 05efde66559d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Get it working in Coq 8.4beta1; use nice coqdoc notation for italics |
files |
changeset | 4b1242b277b2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Typo fixes |
files |
changeset | 057a29f9c773 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Baffling unification messages explained |
files |
changeset | 6413675f8e04 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Recursing under binders in reification |
files |
changeset | 252ba054a1cd |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | One more example of avoiding axioms (getNat) |
files |
changeset | 3322367e955d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Move GeneralRec one chapter slot later, since Subset should be a prereq |
files |
changeset | ad315efc3b6b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Stub out new chapter |
files |
changeset | 518c8994a715 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | One more axiom avoidance example |
files |
changeset | 7466ac31f162 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | New section on avoiding axioms |
files |
changeset | be8c7aae20f4 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass over Universes |
files |
changeset | d5787b70cf48 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Rename Tactics; change 'principal typing' to 'principal types' |
files |
changeset | 7b38729be069 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Tweak mark-up to support coqdoc 8.3 |
files |
changeset | be571572c088 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | PC-inspired Universes tweaks |
files |
changeset | f15f7c4eebfe |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Mention fake universe polymorphism |
files |
changeset | bc0f515a929f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | New release |
files |
changeset | 9dbcd6bad488 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Axioms |
files |
changeset | 2bb1642f597c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Prop section |
files |
changeset | 0be1a42b3035 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Proof-reading pass through first bit of Universes |
files |
changeset | d8c54a25c81f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Update DataStruct with a new reason to use reflexive types; start Universes |
files |