diff src/DataStruct.v @ 475:1fd4109f7b31

Batch of changes based on proofreader feedback
author Adam Chlipala <adam@chlipala.net>
date Mon, 22 Oct 2012 14:23:52 -0400
parents 218361342cd2
children f02b698aadb1
line wrap: on
line diff
--- a/src/DataStruct.v	Mon Oct 22 13:48:45 2012 -0400
+++ b/src/DataStruct.v	Mon Oct 22 14:23:52 2012 -0400
@@ -311,7 +311,7 @@
     | Arrow t1 t2 => typeDenote t1 -> typeDenote t2
   end.
 
-(** Now it is straightforward to write an expression interpreter.  The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values.  An environment for a free variable list [ts] is simply a [hlist typeDenote ts].  That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type.  We use [hget] to implement the [Var] case, and we use [HCons] to extend the environment in the [Abs] case. *)
+(** Now it is straightforward to write an expression interpreter.  The type of the function, [expDenote], tells us that we translate expressions into functions from properly typed environments to final values.  An environment for a free variable list [ts] is simply an [hlist typeDenote ts].  That is, for each free variable, the heterogeneous list that is the environment must have a value of the variable's associated type.  We use [hget] to implement the [Var] case, and we use [HCons] to extend the environment in the [Abs] case. *)
 
 (* EX: Define an interpreter for [exp]s. *)