changeset | 40a9a36844d6 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Batch of changes based on proofreader feedback |
files |
changeset | 417450ccceda |
---|---|
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 | 4320c1a967c2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Spell check |
files |
changeset | 49bd155dfc52 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Proofreading pass through Chapter 8 |
files |
changeset | 2740b8a23cce |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Proofreading pass through Chapter 3 |
files |
changeset | 97c60ffdb998 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Vertical spacing pass for MoreDep and DataStruct |
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 | 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 | 6ed5ee4845e4 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through MoreDep, 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 | ded318830bb0 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Manual font choice for notation scope delimiters |
files |
changeset | f0f76356de9c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Typesetting pass over MoreDep |
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 | b911d0df5eee |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | A pass through Match |
files |
changeset | 31fa03bc0f18 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Get it to build with Coq 8.4 |
files |
changeset | d1276004eec9 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default |
files |
changeset | f7c2bf7f1324 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | The one rule of dependent pattern matching |
files |
changeset | 549d604c3d16 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Move exercises out of mainline book |
files |
changeset | b809d3a8a5b1 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass over old Large material; index fixes |
files |
changeset | ad315efc3b6b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Stub out new chapter |
files |
changeset | c7faf3551c5d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass over MoreDep |
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 | 559ec7328410 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Spelling errors found preparing JFR paper |
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 | 756ce68e42fb |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | PC comments for MoreDep |
files |
changeset | d63cb5fbdce0 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | A suggestion from sbriais: mention that Coq >=8.2 allows omitted match cases |
files |
changeset | d1e0a6d8eef1 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Fix typo |
files |
changeset | 768889c969e9 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Finish porting MoreDep |
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 | cbf2f74a5130 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Parts I want to keep compile with 8.2 |
files |
changeset | 22f111d5cda2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Fix red-black section heading |
files |
changeset | d829cc24faee |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Add a darn newline |
files |
changeset | bc12662ae895 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Exercise added at end of MoreDep |
files |
changeset | 070f4de92311 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Templatize MoreDep |
files |
changeset | 696726af9530 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Prettify rbtree a bit more |
files |
changeset | e579e1e64bde |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Prettify rbtree a bit |
files |
changeset | b78a55b30f4a |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Move [present] section earlier |
files |
changeset | 7804f9d5249f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Correctness of insertion |
files |
changeset | affdf00759d8 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Red-black insert |
files |
changeset | a08e82c646a5 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Comment regexp matcher |
files |
changeset | 41392e5acbf5 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Finish automating regexp |
files |
changeset | 4a57a4922af5 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Add star to regexp matcher; need to automate a bit more |
files |
changeset | 939add5a7db9 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Remove -impredicative-set |
files |
changeset | a0b8b550e265 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Add 'Or' to regexp matcher |
files |
changeset | fd505bcb5632 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of certified regexp matcher |
files |
changeset | 3746a2ded8da |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Tagless interpreter & cfold |
files |
changeset | 522436ed6688 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Incorporate crush' bug reports; ilists in MoreDep |
files |
changeset | d992227e4814 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of MoreDep |
files |