changeset | 306539f29eea |
---|---|
branch | |
bookmark | |
tag | |
user | Arthur Peters <amp@singingwizard.org> |
description | Make specially licensed versions of lib files for cpdtlib.tgz. This adds an ocaml tool and calls to it in the Makefile. |
files |
changeset | d53c077a630c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Make exercises build again |
files |
changeset | d65e9c1c9041 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Touch-ups in 8.4 |
files |
changeset | ed829eaa91b2 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Builds with Coq 8.5beta2 |
files |
changeset | 136d4b84eb96 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Build an open-source release of library modules |
files |
changeset | 929c12a95b87 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Add back in external LaTeX links |
files |
changeset | a95af5a59990 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Exercises online |
files |
changeset | 39c204d2262c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Remove hyperlinks to standard library, which were broken anyway |
files |
changeset | e2c88317611f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Conclusion |
files |
changeset | d5112c099fbf |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | New chapter: ProgLang |
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 | 21229271f44c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Fix 'make clean' |
files |
changeset | d5787b70cf48 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Rename Tactics; change 'principal typing' to 'principal types' |
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 | 690796f4690d |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | Further emphasize necessity and purpose of Set Implicit Arguments; tweak Makefile to support parallel builds |
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 | 693897f8e0cb |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adam@chlipala.net> |
description | PC comments for DataStruct |
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 | 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 | 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 | 9d0b9577f8b1 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | First 8.2 release |
files |
changeset | dbac52f5bce1 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Port Generic |
files |
changeset | 6601384e7e14 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Touch-ups to DataStruct |
files |
changeset | f8bcd33bdd91 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Port DataStruct |
files |
changeset | 768889c969e9 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Finish porting MoreDep |
files |
changeset | 3227be370687 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Ported Subset |
files |
changeset | b149a07b9b5b |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Most old Sestoft suggestions processed |
files |
changeset | b9e9ff52913c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Port InductiveTypes |
files |
changeset | 3f4576f15130 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Revising for 8.2 through first big example |
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 | a2b14ba218a7 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Typo reported by mulhern; stop publishing to Harvard |
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 | 022feabdff50 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | STLC cpsExp |
files |
changeset | 7fd470d8a788 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | System F |
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 |
changeset | 8157e8e28e2e |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Proved concrete substitution |
files |
changeset | 6a00d49e85fb |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of Reflection |
files |
changeset | bc1f7d3687e7 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of Match |
files |
changeset | 8a548a6c7074 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Add ext_eq axiom and DepList notations |
files |
changeset | ee676bf3d681 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Up to Streicher |
files |
changeset | 2f97c8177172 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | DepList |
files |
changeset | ec0fb0f00f46 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of DataStruct |
files |
changeset | 939add5a7db9 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Remove -impredicative-set |
files |
changeset | d992227e4814 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of MoreDep |
files |
changeset | c49d999fe806 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | MoreSpecif |
files |
changeset | 1e3c49602384 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Start of Subset |
files |
changeset | de9f78d68053 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Publish to Harvard, too |
files |