Mercurial > cpdt > repo
diff src/DeBruijn.v @ 291:da9ccc6bf572
PC comments for DeBruijn
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Wed, 10 Nov 2010 15:42:05 -0500 |
parents | dce88a5c170c |
children | 7b38729be069 |
line wrap: on
line diff
--- a/src/DeBruijn.v Wed Nov 10 15:37:01 2010 -0500 +++ b/src/DeBruijn.v Wed Nov 10 15:42:05 2010 -0500 @@ -1,4 +1,4 @@ -(* Copyright (c) 2009, Adam Chlipala +(* Copyright (c) 2009-2010, Adam Chlipala * * This work is licensed under a * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 @@ -150,7 +150,7 @@ end). (* end hide *) -(** Less than a page of tactic code will be sufficient to automate our proof of commuativity. We start by defining a workhorse simplification tactic [simp], which extends [crush] in a few ways. +(** Less than a page of tactic code will be sufficient to automate our proof of commutativity. We start by defining a workhorse simplification tactic [simp], which extends [crush] in a few ways. [[ Ltac simp := repeat progress (crush; try discriminate;