changeset | 49f3b2d70302 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through Chapter 14 |
files |
changeset | 31258618ef73 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Incorporate feedback from Nathan Collins |
files |
changeset | 5025a401ad9e |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Last round of feedback from class at Penn |
files |
changeset | 582cf453878e |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Update Match to take into account a number of misunderstandings of tactic execution in 8.4 and 8.4pl1 |
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 | 38549f152568 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Proofreading pass through Chapter 14 |
files |
changeset | 0650420c127b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Finished vertical spacing |
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 | 85e743564b22 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through Match, to incorporate new coqdoc features |
files |
changeset | 078edca127cf |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Typesetting pass over Match |
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 | cc8d0503619f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Citations for continuations and unification |
files |
changeset | b911d0df5eee |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | A pass through Match |
files |
changeset | 549d604c3d16 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Move exercises out of mainline book |
files |
changeset | 50e1d338728c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | First draft of full prose for GeneralRec |
files |
changeset | 23b06f87bd30 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | More coqdoc bug workarounds |
files |
changeset | 386b7ad8849b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Change some template annotations |
files |
changeset | 2eeb96aa0426 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Finish adding Match exercises |
files |
changeset | 49c6aa7d2148 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Another Match exercise |
files |
changeset | d7178fb77321 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Two exercises for Match |
files |
changeset | cbeccef45f4e |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass over Match |
files |
changeset | 06d11a6363cd |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | New LogicProg chapter |
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 | f4768d5a75eb |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Typo fix |
files |
changeset | b441010125d4 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Everything compiles in Coq 8.3pl1 |
files |
changeset | b653e6b19b6d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | PC comments for Match |
files |
changeset | 82eae7bc91ea |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Working with evars |
files |
changeset | 15501145d696 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Ported Match |
files |
changeset | f05514cc6c0d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | 'make doc' works with 8.2 |
files |
changeset | cbf2f74a5130 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Parts I want to keep compile with 8.2 |
files |
changeset | ce4cc7fa9b2b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Templatize Match |
files |
changeset | 8cce3247496b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Prose for matcher |
files |
changeset | a9e90bacbd16 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | inster example |
files |
changeset | 59a2110acf64 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Uncommented matcher code |
files |
changeset | c0bda476b44b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Functional programming in Ltac |
files |
changeset | d6b1e9de7fc1 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Free variables in unification variables issue |
files |
changeset | 091583baf345 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Through completer' |
files |
changeset | f9d8f33c9b46 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | autorewrite |
files |
changeset | 28ef7f0da085 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | auto |
files |
changeset | bc1f7d3687e7 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of Match |
files |