changeset | ed829eaa91b2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Builds with Coq 8.5beta2 |
files |
changeset | 8921cfa2f503 |
---|---|
branch | |
bookmark | |
tag | |
user | Cl?ment Pit--Claudel <clement.pitclaudel@live.com> |
description | Use TeX magic to prevent -- from being displayed as an en dash |
files |
changeset | b7419a10e52e |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through Chapter 6 |
files |
changeset | 1fd4109f7b31 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Batch of changes based on proofreader feedback |
files |
changeset | d9e1fb184672 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Batch of changes based on proofreader feedback |
files |
changeset | 51a8472aca68 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Batch of changes based on proofreader feedback |
files |
changeset | b36876d4611e |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Batch of changes based on proofreader feedback |
files |
changeset | 822442bf6d7f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Proofreading pass through Chapter 5 |
files |
changeset | 2740b8a23cce |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Proofreading pass through Chapter 3 |
files |
changeset | 89c67796754e |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Undo some overzealous vspace tweaks |
files |
changeset | f923024bd284 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Vertical spacing pass, through end of Subset |
files |
changeset | 393b8ed99c2f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | A pass of improvements to vertical spacing, up through end of InductiveTypes |
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 | 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 | d3a40c044ab4 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through Subset, to incorporate new coqdoc features |
files |
changeset | 1edeec5d5d0c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Typesetting pass over Subset |
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 | 31fa03bc0f18 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Get it to build with Coq 8.4 |
files |
changeset | 549d604c3d16 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Move exercises out of mainline book |
files |
changeset | e76aced46eb1 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Typo fix |
files |
changeset | aaeba4cfd075 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Work around coqdoc bug |
files |
changeset | c7faf3551c5d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass over MoreDep |
files |
changeset | 4186722d329b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Hide some more Subset code in template |
files |
changeset | 1f57a8d0ed3d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass over Subset |
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 | b441010125d4 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Everything compiles in Coq 8.3pl1 |
files |
changeset | 1b6c81e51799 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Fixes added while proofreading JFR camera-ready |
files |
changeset | 2c88fc1dbe33 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | A pass of double-quotes and LaTeX operator beautification |
files |
changeset | caa69851c78d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Subset suggestions from PC; improvements to build process for coqdoc fontification |
files |
changeset | aa3c054afce0 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Some bug fixes while working on JFR version |
files |
changeset | c4b1c0de7af9 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of MoreDep port; new [dep_destruct] based on [dependent destruction] |
files |
changeset | 3227be370687 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Ported Subset |
files |
changeset | cbf2f74a5130 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Parts I want to keep compile with 8.2 |
files |
changeset | 939add5a7db9 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Remove -impredicative-set |
files |
changeset | 15e2b3485dc4 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Subset exercises |
files |
changeset | d07c77659c20 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Templatizing Subset |
files |
changeset | 82a2189fa283 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Spell check |
files |
changeset | ec2c1830a7a1 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Type-checking example, with discussion |
files |
changeset | a21447f76aad |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Break into Parts |
files |
changeset | 535e1cd17d9a |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | maybe and sumor |
files |
changeset | 839d159cac5d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Code for type-checking example |
files |
changeset | db967eff40d7 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | sumbool |
files |
changeset | 1e3c49602384 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of Subset |
files |