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;