Mercurial > cpdt > repo
changeset 291:da9ccc6bf572
PC comments for DeBruijn
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 10 Nov 2010 15:42:05 -0500 |
| parents | 758778c0468c |
| children | 2c88fc1dbe33 |
| files | src/DeBruijn.v |
| diffstat | 1 files changed, 2 insertions(+), 2 deletions(-) [+] |
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;