<div class="gmail_quote">On Fri, Aug 21, 2009 at 2:11 PM, Matthew Fluet <span dir="ltr"><<a href="mailto:fluet@tti-c.org">fluet@tti-c.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">
The concept is fine, but... it might be better to ... rebind elements of an _EXTRA structure.</blockquote></div><br>Revised and committed.<br><br>