log src/StackMachine.v

age author description
Wed, 06 Jun 2012 11:25:13 -0400 Adam Chlipala Get it working in Coq 8.4beta1; use nice coqdoc notation for italics
Sun, 22 Apr 2012 15:51:03 -0400 Adam Chlipala Citations for continuations and unification
Mon, 26 Mar 2012 16:55:59 -0400 Adam Chlipala Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default
Thu, 03 Nov 2011 17:04:41 -0400 Adam Chlipala Explicit note about primitive recursion restriction, early on
Sun, 25 Sep 2011 13:20:56 -0400 Adam Chlipala Pass over Match
Sun, 11 Sep 2011 17:22:36 -0400 Adam Chlipala Pass through InductiveTypes, through end of reflexive types
Wed, 07 Sep 2011 13:47:24 -0400 Adam Chlipala Rename Tactics; change 'principal typing' to 'principal types'
Thu, 01 Sep 2011 11:32:15 -0400 Adam Chlipala Pass through second half of StackMachine
Mon, 29 Aug 2011 15:31:06 -0400 Adam Chlipala Pass through first half of StackMachine, along with some reorganization of the build process
Thu, 25 Aug 2011 14:41:49 -0400 Adam Chlipala Finished 2011 pass through Intro
Wed, 03 Aug 2011 10:34:53 -0400 Adam Chlipala Further emphasize necessity and purpose of Set Implicit Arguments; tweak Makefile to support parallel builds
Tue, 28 Jun 2011 08:38:08 -0400 Adam Chlipala Clarify need to insert hidden commands
Mon, 17 Jan 2011 15:12:30 -0500 Adam Chlipala Tweak mark-up to support coqdoc 8.3
Fri, 14 Jan 2011 14:55:32 -0500 Adam Chlipala Small tweak to keep things working in 8.2
Thu, 09 Dec 2010 13:44:57 -0500 Adam Chlipala Fixes added while proofreading JFR camera-ready
Wed, 10 Nov 2010 16:31:04 -0500 Adam Chlipala A pass of double-quotes and LaTeX operator beautification
Fri, 01 Oct 2010 14:19:20 -0400 Adam Chlipala Incorporate PC's comments on InductiveTypes
Fri, 01 Oct 2010 13:39:05 -0400 Adam Chlipala Some improvements to installation instructions, based on Mitch Wand's feedback
Tue, 21 Sep 2010 09:50:33 -0400 Adam Chlipala PC comments for Chapter 2
Sat, 15 May 2010 06:42:05 -0400 Adam Chlipala Typo pointed out by Ben Moseley
Wed, 03 Feb 2010 08:14:39 -0500 Adam Chlipala Fix PDF ToC generation; mention Set Implicit Arguments in StackMachine
Mon, 09 Nov 2009 13:18:46 -0500 Adam Chlipala Most old Sestoft suggestions processed
Fri, 06 Nov 2009 17:10:27 -0500 Adam Chlipala Converted StackMachine
Fri, 06 Nov 2009 16:44:06 -0500 Adam Chlipala Revising for 8.2 through first big example
Fri, 06 Nov 2009 12:15:05 -0500 Adam Chlipala 'make doc' works with 8.2
Sat, 03 Jan 2009 19:57:02 -0500 Adam Chlipala Feedback from Peter Gammie
Tue, 07 Oct 2008 10:50:36 -0400 Adam Chlipala Remove -impredicative-set from text
Tue, 16 Sep 2008 16:18:11 -0400 Adam Chlipala Small prose change
Sat, 13 Sep 2008 08:58:48 -0400 Adam Chlipala Spell check
Mon, 08 Sep 2008 15:38:34 -0400 Adam Chlipala Parameterized inductives
Mon, 08 Sep 2008 14:19:50 -0400 Adam Chlipala Start of Inductive Types
Mon, 08 Sep 2008 12:42:57 -0400 Adam Chlipala Real chapter titles; describe how to get Proof General to use command-line flags
Fri, 05 Sep 2008 16:46:32 -0400 Adam Chlipala Template generation
Wed, 03 Sep 2008 16:14:47 -0400 Adam Chlipala Finished typed example
Wed, 03 Sep 2008 15:59:37 -0400 Adam Chlipala Translation
Wed, 03 Sep 2008 15:39:41 -0400 Adam Chlipala Typed target denotation
Wed, 03 Sep 2008 15:08:28 -0400 Adam Chlipala Target language source examples
Wed, 03 Sep 2008 15:05:21 -0400 Adam Chlipala Source language examples
Wed, 03 Sep 2008 15:00:56 -0400 Adam Chlipala Source language semantics
Wed, 03 Sep 2008 14:26:52 -0400 Adam Chlipala Typed expression language
Wed, 03 Sep 2008 13:45:59 -0400 Adam Chlipala Merge; make prose nicer base book/src/StackMachine.v@fc68277d91d2
Wed, 03 Sep 2008 13:30:05 -0400 Adam Chlipala Squash book into main directory base book/src/StackMachine.v@3dfe06986c73