local refs

[Matthew Fluet]

> multiThreaded: Label.t -> Bool.t
> labelOfBlockContaining: Use.t -> Label.t
> 
> (forall uses u of x, 
>    multiThreaded(labelOfBlockContaining(u)) ==> u is Ref_assign)
> or (forall uses u of x
>       multiThreaded(labelOfBlockContaining(u)) ==> u is Ref_deref)

Ok.  I accept this as a definition that rejects the program I proposed.
But, I don't really think it's the right notion for flattening of refs;
your next e-mail seems to capture it better.