--- a/src/LogicProg.v	Tue Apr 07 18:59:24 2015 -0400
+++ b/src/LogicProg.v	Wed Aug 05 14:46:55 2015 -0400
@@ -1,4 +1,4 @@
-(* Copyright (c) 2011-2012, Adam Chlipala
+(* Copyright (c) 2011-2012, 2015, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -9,12 +9,12 @@
 
 (* begin hide *)
 
-Require Import List.
+Require Import List Omega.
 
-Require Import CpdtTactics.
+Require Import Cpdt.CpdtTactics.
 
 Set Implicit Arguments.
-
+Set Asymmetric Patterns.
 (* end hide *)
 
 (** %\part{Proof Engineering}
@@ -685,12 +685,6 @@
 Qed.
 (* end thide *)
 
-(* begin hide *)
-(* begin thide *)
-Definition e1s := eval1'_subproof.
-(* end thide *)
-(* end hide *)
-
 Print eval1'.
 (** %\vspace{-.15in}%[[
 eval1' =