log src/Universes.v

age author description
Wed, 12 Jul 2017 13:08:24 -0400 Adam Chlipala Fixes for Coq 8.6
Wed, 05 Aug 2015 14:46:55 -0400 Adam Chlipala Builds with Coq 8.5beta2
Wed, 13 Feb 2013 10:22:18 -0500 Adam Chlipala Finished last pass through the book before beginning the MIT Press editorial process
Sun, 10 Feb 2013 15:40:28 -0500 Adam Chlipala Pass through Chapter 12
Tue, 08 Jan 2013 14:38:56 -0500 Adam Chlipala Incorporate feedback from Nathan Collins
Wed, 28 Nov 2012 19:33:21 -0500 Adam Chlipala Batch of changes based on proofreader feedback
Mon, 22 Oct 2012 14:23:52 -0400 Adam Chlipala Batch of changes based on proofreader feedback
Tue, 28 Aug 2012 16:53:16 -0400 Adam Chlipala Proofreading pass through Chapter 12
Wed, 01 Aug 2012 17:03:39 -0400 Adam Chlipala Vertical spacing through end of Part II
Fri, 27 Jul 2012 16:47:28 -0400 Adam Chlipala A pass over all formatting, after big pile of coqdoc changes
Fri, 27 Jul 2012 15:41:06 -0400 Adam Chlipala Changes during more coqdoc hacking
Thu, 26 Jul 2012 19:05:12 -0400 Adam Chlipala Changes while hacking on coqdoc
Thu, 26 Jul 2012 11:55:52 -0400 Adam Chlipala Pass through Universes, to incorporate new coqdoc features
Wed, 25 Jul 2012 18:10:26 -0400 Adam Chlipala Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]
Wed, 25 Jul 2012 15:51:54 -0400 Adam Chlipala Pass through StackMachine, to incorporate new coqdoc features
Tue, 17 Jul 2012 16:37:58 -0400 Adam Chlipala Update for Coq trunk version intended for final 8.4 release
Fri, 08 Jun 2012 15:00:59 -0400 Adam Chlipala Typesetting pass over Universes
Wed, 06 Jun 2012 11:25:13 -0400 Adam Chlipala Get it working in Coq 8.4beta1; use nice coqdoc notation for italics
Fri, 20 Apr 2012 12:49:47 -0400 Adam Chlipala Typo fixes
Thu, 12 Apr 2012 16:27:28 -0400 Adam Chlipala Baffling unification messages explained
Thu, 29 Mar 2012 17:13:23 -0400 Adam Chlipala Recursing under binders in reification
Wed, 28 Mar 2012 13:20:50 -0400 Adam Chlipala One more example of avoiding axioms (getNat)
Wed, 26 Oct 2011 17:14:28 -0400 Adam Chlipala Move GeneralRec one chapter slot later, since Subset should be a prereq
Wed, 26 Oct 2011 11:19:52 -0400 Adam Chlipala Stub out new chapter
Wed, 19 Oct 2011 10:00:07 -0400 Adam Chlipala One more axiom avoidance example
Mon, 17 Oct 2011 14:56:46 -0400 Adam Chlipala New section on avoiding axioms
Mon, 17 Oct 2011 11:09:23 -0400 Adam Chlipala Pass over Universes
Wed, 07 Sep 2011 13:47:24 -0400 Adam Chlipala Rename Tactics; change 'principal typing' to 'principal types'
Mon, 17 Jan 2011 15:12:30 -0500 Adam Chlipala Tweak mark-up to support coqdoc 8.3
Wed, 10 Nov 2010 14:05:00 -0500 Adam Chlipala PC-inspired Universes tweaks
Mon, 30 Nov 2009 14:21:34 -0500 Adam Chlipala Mention fake universe polymorphism
Mon, 23 Nov 2009 12:41:14 -0500 Adam Chlipala New release
Mon, 23 Nov 2009 11:33:22 -0500 Adam Chlipala Axioms
Fri, 20 Nov 2009 11:02:26 -0500 Adam Chlipala Prop section
Fri, 20 Nov 2009 10:18:35 -0500 Adam Chlipala Proof-reading pass through first bit of Universes
Wed, 18 Nov 2009 15:38:01 -0500 Adam Chlipala Update DataStruct with a new reason to use reflexive types; start Universes