changeset | ed829eaa91b2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Builds with Coq 8.5beta2 |
files |
changeset | 7d2339cbd39c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through Chapter 10 |
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 | f38a3af9dd17 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Batch of changes based on proofreader feedback |
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 | 4320c1a967c2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Spell check |
files |
changeset | 848bf35f7f6c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Proofreading pass through Chapter 10 |
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 | 5e6b76ca14de |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through Equality, 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 | ff0aef0f33a5 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Typesetting pass over Equality |
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 | bef6fb896edd |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | More discussion of axiom avoidance and tactic pitfalls for JMeq |
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 | 990151eac6af |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Discuss reduction of [fix] |
files |
changeset | 2fbb47fb02bd |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through old content of Equality |
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 | 123f466faedc |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Small tweak to keep things working in 8.2 |
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 | 540a09187193 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | PC changes to Equality and Generic |
files |
changeset | bd7f8720a691 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Typo fix |
files |
changeset | 19fbda8a8117 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Typo fix in Equality, found proof-reading tutorial |
files |
changeset | aa3c054afce0 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Some bug fixes while working on JFR version |
files |
changeset | c8508d277a00 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Ported Equality |
files |
changeset | f05514cc6c0d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | 'make doc' works with 8.2 |
files |
changeset | cadeb49dc1ef |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Fix typo |
files |
changeset | bc1f7d3687e7 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of Match |
files |
changeset | 6bf40eff5e98 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | call-by-name is really call-by-need |
files |
changeset | 0bfc75502498 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Equality exercise |
files |
changeset | 57eaceb085f6 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Templatize Equality |
files |
changeset | 9ccd215e5112 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | ext_eq |
files |
changeset | 7cbf0376702f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Definitional equality |
files |
changeset | 61e5622b1195 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Interconvertibility |
files |
changeset | 39c7894b3f7f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | JMeq |
files |
changeset | 8df59f0b3dc0 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Proofs with equality |
files |
changeset | ee676bf3d681 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Up to Streicher |
files |