--- a/src/StackMachine.v	Wed Aug 01 15:52:50 2012 -0400
+++ b/src/StackMachine.v	Wed Aug 01 16:09:37 2012 -0400
@@ -103,6 +103,9 @@
 Eval simpl in expDenote (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
 (** [= 28 : nat] *)
 
+(** %\smallskip{}%Nothing too surprising goes on here, so we are ready to move on to the target language of our compiler. *)
+
+
 (** ** Target Language *)
 
 (** We will compile our source programs onto a simple stack machine, whose syntax is: *)
@@ -140,6 +143,8 @@
       end
   end.
 
+(** With the two programming languages defined, we can turn to the compiler definition. *)
+
 
 (** ** Translation *)
 
@@ -163,7 +168,7 @@
 Eval simpl in compile (Binop Times (Binop Plus (Const 2) (Const 2)) (Const 7)).
 (** [= iConst 7 :: iConst 2 :: iConst 2 :: iBinop Plus :: iBinop Times :: nil : prog] *)
 
-(** We can also run our compiled programs and check that they give the right results. *)
+(** %\smallskip{}%We can also run our compiled programs and check that they give the right results. *)
 
 Eval simpl in progDenote (compile (Const 42)) nil.
 (** [= Some (42 :: nil) : option stack] *)
@@ -615,10 +620,12 @@
   (TNConst 7)).
 (** [= true : typeDenote Bool] *)
 
+(** %\smallskip{}%Now we are ready to define a suitable stack machine target for compilation. *)
+
 
 (** ** Target Language *)
 
-(** Now we want to define a suitable stack machine target for compilation.  In the example of the untyped language, stack machine programs could encounter stack underflows and "get stuck."  This was unfortunate, since we had to deal with this complication even though we proved that our compiler never produced underflowing programs.  We could have used dependent types to force all stack machine programs to be underflow-free.
+(** In the example of the untyped language, stack machine programs could encounter stack underflows and "get stuck."  This was unfortunate, since we had to deal with this complication even though we proved that our compiler never produced underflowing programs.  We could have used dependent types to force all stack machine programs to be underflow-free.
 
 For our new languages, besides underflow, we also have the problem of stack slots with naturals instead of bools or vice versa.  This time, we will use indexed typed families to avoid the need to reason about potential failures.
 
@@ -761,6 +768,8 @@
   (TNConst 7)) nil) tt.
 (** [= (true, tt) : vstack (Bool :: nil)] *)
 
+(** %\smallskip{}%The compiler seems to be working, so let us turn to proving that it _always_ works. *)
+
 
 (** ** Translation Correctness *)