changeset | 2a2a6a0241b5 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Add copyright year |
files |
changeset | 16d701d4bd82 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | And working with 8.6 again |
files |
changeset | 71b85aaae868 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Fix Epigram URL |
files |
changeset | dac7a2705b00 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | ...and back to working in 8.4 again |
files |
changeset | ed829eaa91b2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Builds with Coq 8.5beta2 |
files |
changeset | 6b3fb6672cfa |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Addressing some inaccuracies of comparison with PVS |
files |
changeset | da576746c3ba |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Fix one reported grammatical error and make my own final pass over Chapter 1 |
files |
changeset | a95af5a59990 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Exercises online |
files |
changeset | 8bfb27cf0121 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Add explicit warning that Coq 8.4 or later is required |
files |
changeset | 6769ef9688f2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Updated description of CoqIDE limitations |
files |
changeset | 1fd4109f7b31 |
---|---|
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 | 4320c1a967c2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Spell check |
files |
changeset | a0c604da96d3 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Proofreading pass through Chapter 1 |
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 | 686cf945dd02 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through StackMachine, to incorporate new coqdoc features |
files |
changeset | eda5f4eb21b4 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Improve Intro mark-up, based on new coqdoc features planned for final 8.4 release |
files |
changeset | 5986e9fd40b5 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Start figuring out which coqdoc changes will be needed to produce a pretty final version |
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 | d62ed7381a0b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Instructions on directory-local Coq parameter specification, thanks to a tip from Thomas Braibant |
files |
changeset | d40b05266306 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Define 'certified program' |
files |
changeset | 76e1dfcb86eb |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Comment CpdtTactics.v |
files |
changeset | 9e47cdd76bb5 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Typo fixes |
files |
changeset | d5112c099fbf |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | New chapter: ProgLang |
files |
changeset | 31fa03bc0f18 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Get it to build with Coq 8.4 |
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 | 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 | 4a432659a698 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Remove Part IV |
files |
changeset | 06d11a6363cd |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | New LogicProg chapter |
files |
changeset | 70e51e8cfce7 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | New InductiveTypes exercises and difficulty markings |
files |
changeset | d5787b70cf48 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Rename Tactics; change 'principal typing' to 'principal types' |
files |
changeset | 495153a41819 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through second half of StackMachine |
files |
changeset | 4cb3ba8604bc |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Pass through first half of StackMachine, along with some reorganization of the build process |
files |
changeset | d2cb78f54454 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Finished 2011 pass through Intro |
files |
changeset | a419a60e5ff6 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Started revising Intro |
files |
changeset | 25ec92be5ad2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Forgot to increment two timestamps |
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 | 4146889930c5 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | PC's Chapter 5 comments |
files |
changeset | fabbc71abd80 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Incorporate PC's comments on InductiveTypes |
files |
changeset | e7ed2fddd29a |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Some improvements to installation instructions, based on Mitch Wand's feedback |
files |
changeset | 191a66cd7cb5 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Fix PDF ToC generation; mention Set Implicit Arguments in StackMachine |
files |
changeset | dce88a5c170c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Import DeBruijn |
files |
changeset | de53c8bcfa8d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | OpSem code |
files |
changeset | 0400fa005d5a |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | New release |
files |
changeset | 52b9e43be069 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Uncommented functor example |
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 |
changeset | dbac52f5bce1 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Port Generic |
files |
changeset | b149a07b9b5b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Most old Sestoft suggestions processed |
files |
changeset | 3f4576f15130 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Revising for 8.2 through first big example |
files |
changeset | 8e9499e27b6c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of Generic |
files |
changeset | 094bd1e353dd |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Import predicative Impure example |
files |
changeset | 24b99e025fe8 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of Intensional |
files |
changeset | ec44782bffdd |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Extensional exercise |
files |
changeset | 022feabdff50 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | STLC cpsExp |
files |
changeset | f8353e2a21d6 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | STLC example in Interps |
files |
changeset | fabfaa93c9ea |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Hoas, up to type soundness |
files |