# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1289421725 18000
# Node ID da9ccc6bf572d182cc9fd9422d556c2c7e6eb30d
# Parent  758778c0468ccedf2417a10d31bbf61c6a44c5d4
PC comments for DeBruijn

diff -r 758778c0468c -r da9ccc6bf572 src/DeBruijn.v
--- 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;