--- a/src/Large.v	Fri Aug 17 15:39:55 2012 -0400
+++ b/src/Large.v	Thu Aug 23 11:06:37 2012 -0400
@@ -49,7 +49,7 @@
     | Plus e1 e2 => Plus (times k e1) (times k e2)
   end.
 
-(** We can write a very manual proof that [double] really doubles an expression's value. *)
+(** We can write a very manual proof that [times] really implements multiplication. *)
 
 Theorem eval_times : forall k e,
   eval (times k e) = k * eval e.

--- a/src/StackMachine.v	Fri Aug 17 15:39:55 2012 -0400
+++ b/src/StackMachine.v	Thu Aug 23 11:06:37 2012 -0400
@@ -550,7 +550,7 @@
 
 (** The definition of [tbinop] is different from [binop] in an important way.  Where we declared that [binop] has type [Set], here we declare that [tbinop] has type [type -> type -> type -> Set].  We define [tbinop] as an _indexed type family_.  Indexed inductive types are at the heart of Coq's expressive power; almost everything else of interest is defined in terms of them.
 
-The inuitive explanation of [tbinop] is that a [tbinop t1 t2 t] is a binary operator whose operands should have types [t1] and [t2], and whose result has type [t].  For instance, constructor [TLt] (for less-than comparison of numbers) is assigned type [tbinop Nat Nat Bool], meaning the operator's arguments are naturals and its result is Boolean.  The type of [TEq] introduces a small bit of additional complication via polymorphism: we want to allow equality comparison of any two values of any type, as long as they have the _same_ type.
+The intuitive explanation of [tbinop] is that a [tbinop t1 t2 t] is a binary operator whose operands should have types [t1] and [t2], and whose result has type [t].  For instance, constructor [TLt] (for less-than comparison of numbers) is assigned type [tbinop Nat Nat Bool], meaning the operator's arguments are naturals and its result is Boolean.  The type of [TEq] introduces a small bit of additional complication via polymorphism: we want to allow equality comparison of any two values of any type, as long as they have the _same_ type.
 
 ML and Haskell have indexed algebraic datatypes.  For instance, their list types are indexed by the type of data that the list carries.  However, compared to Coq, ML and Haskell 98 place two important restrictions on datatype definitions.