diff src/StackMachine.v @ 465:4320c1a967c2

Spell check
author Adam Chlipala <adam@chlipala.net>
date Wed, 29 Aug 2012 18:26:26 -0400
parents 980962258b49
children b4dd18787d04
line wrap: on
line diff
--- a/src/StackMachine.v	Wed Aug 29 17:17:17 2012 -0400
+++ b/src/StackMachine.v	Wed Aug 29 18:26:26 2012 -0400
@@ -694,7 +694,7 @@
  while it is expected to have type "vstack ?119".
 >>
 
-This and other mysteries of Coq dependent typing we postpone until Part II of the book.  The upshot of our later discussion is that it is often useful to push inside of [match] branches those function parameters whose types depend on the type of the value being matched.  Our later, more complete treatement of Gallina's typing rules will explain why this helps.
+This and other mysteries of Coq dependent typing we postpone until Part II of the book.  The upshot of our later discussion is that it is often useful to push inside of [match] branches those function parameters whose types depend on the type of the value being matched.  Our later, more complete treatment of Gallina's typing rules will explain why this helps.
 *)
 
 (** We finish the semantics with a straightforward definition of program denotation. *)