| Fri, 14 Jan 2011 14:39:12 -0500 |
Adam Chlipala |
Everything compiles in Coq 8.3pl1 |
| Mon, 28 Dec 2009 12:35:44 -0500 |
Adam Chlipala |
OpSem code |
| Wed, 16 Dec 2009 15:31:54 -0500 |
Adam Chlipala |
Prosified Extensional |
| Wed, 11 Nov 2009 10:27:47 -0500 |
Adam Chlipala |
Start of MoreDep port; new [dep_destruct] based on [dependent destruction] |
| Fri, 06 Nov 2009 10:52:43 -0500 |
Adam Chlipala |
Parts I want to keep compile with 8.2 |
| Fri, 02 Jan 2009 08:57:25 -0500 |
Adam Chlipala |
Small fixes while reading student solutions |
| Sun, 16 Nov 2008 15:04:21 -0500 |
Adam Chlipala |
About to stop using JMeq |
| Sun, 16 Nov 2008 14:01:33 -0500 |
Adam Chlipala |
Closure conversion defined |
| Mon, 10 Nov 2008 14:12:22 -0500 |
Adam Chlipala |
PatMatch Elaborate_correct |
| Mon, 10 Nov 2008 11:36:00 -0500 |
Adam Chlipala |
CpsExp_correct |
| Sun, 09 Nov 2008 15:15:41 -0500 |
Adam Chlipala |
System F |
| Mon, 03 Nov 2008 14:47:46 -0500 |
Adam Chlipala |
Interderivability of big and small step |
| Sat, 18 Oct 2008 12:04:28 -0400 |
Adam Chlipala |
Up to Streicher |
| Wed, 08 Oct 2008 09:41:50 -0400 |
Adam Chlipala |
crush' pursues trivial inversions |
| Tue, 07 Oct 2008 10:43:54 -0400 |
Adam Chlipala |
Get Coinductive compiling again |
