New patches:

[unrevert
anon**20121226072947
 Ignore-this: 25945a653db3d170ba43648711d483b5
] hunk ./devel/Iron/Language/SystemF2Effect/TyJudge.v 10
 Require Import Iron.Language.SystemF2Effect.VaExpLift.
 
 
-(* Store Environment holds the types of locations. *)
+(* Store Environment holds the type of each location. *)
 Definition stenv := list ty.
 
 
hunk ./devel/Iron/Language/SystemF2Effect/TyJudge.v 17
 (* Types of Value expressions *)
 Inductive TYPEV : kienv -> tyenv -> stenv -> val -> ty -> Prop := 
   | TvVar
-    :  forall ke te se i t
+    :  forall ke te se rei t
     ,  get i te = Some t
hunk ./devel/Iron/Language/SystemF2Effect/TyJudge.v 19
-    -> TYPEV ke te se (VVar i) t 
+    -> TYPEV ke te se re (VVar i) t 
 
   | TvLoc 
hunk ./devel/Iron/Language/SystemF2Effect/TyJudge.v 22
-    :  forall ke te se i t
-    ,  get i se  = Some t
-    -> TYPEV ke te se (VLoc i) t
+    :  forall ke te se re iLoc iRegion tLoc
+    ,  get iLoc se  = Some tLoc
+    ,  get 
+    -> TYPEV ke te se re (VLoc iLoc) (tRef (TVar iRegion) tLoc)
 
   | TvLam
     :  forall ke te se t1 t2 x2 e2
hunk ./devel/Iron/Language/SystemF2Effect/TyJudge.v 141
       -> t1 = t1');
   intros; try (solve [inverts_type; try congruence]).
 
+ Case "VLoc".
+  inverts_type. unfold tRef.
+  rewrite H5 in H4. inverts H4. eauto.
+
  Case "VLam".
   inverts_type. spec IHx H8 H9. burn.
 

Context:

[F2Effect: Add single step rules
Ben Lippmeier <benl@ouroborus.net>**20121226063222
 Ignore-this: 41c34f33d9e4099d672a2b229430120c
] 
[Finish README
Ben Lippmeier <benl@ouroborus.net>**20121224101515
 Ignore-this: 1a53233f5905b35dc5bafc3f02d18793
] 
[Remove SimpleResource proof, not enough finished to worry about.
Ben Lippmeier <benl@ouroborus.net>**20121224100646
 Ignore-this: 59ae29934c4ad20e4befeccb364c1c78
] 
[Start on LICENSE and README
Ben Lippmeier <benl@ouroborus.net>**20121224100613
 Ignore-this: a76941f5d8607fbf3a2684d559ba0608
] 
[Fixup imports and makefile
Ben Lippmeier <benl@ouroborus.net>**20121224091744
 Ignore-this: d170a54f3b3de66551cfd9564f3c9430
] 
[Import DiscipleKernel, SimplePCFa, SimpleResource, SystemF2Effect
Ben Lippmeier <benl@ouroborus.net>**20121224090050
 Ignore-this: 5044d1284df61e237a8319ac2f28bcba
] 
[Import SystemF, SystemF2, SystemF2Data and SystemF2Store
Ben Lippmeier <benl@ouroborus.net>**20121224085716
 Ignore-this: 9de85cbe4c063db811376e9e8c4a3f2f
] 
[Import SimpleData, SimplePCF and SimpleRef
Ben Lippmeier <benl@ouroborus.net>**20121224065635
 Ignore-this: 1d7935cdd9a528b685413116648ba03c
] 
[Simple: formatting wibbles
Ben Lippmeier <benl@ouroborus.net>**20121224061901
 Ignore-this: bb445d6140d87117d2c4117850d1a2b9
] 
[Import framework and Simple proof from DDC tree
Ben Lippmeier <benl@ouroborus.net>**20121224055827
 Ignore-this: 538ef4c179313b75d76d46c8419b9d91
] 
Patch bundle hash:
a728489afd58e84e0598ced614872eb09e104f22