Mercurial > cpdt > repo
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. *)