<div class="gmail_extra"><div class="gmail_quote">On Fri, Dec 7, 2012 at 4:23 PM, Juan Jose Garcia-Ripoll <span dir="ltr"><<a href="mailto:juanjose.garciaripoll@gmail.com" target="_blank">juanjose.garciaripoll@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="gmail_extra">Not really. Seems the type propagator is confused about it -- could you please open a bug report for this? Thanks!</div>
<br></blockquote></div><br clear="all">Done.<br>-- <br>Jerry James<br><a href="http://www.jamezone.org/">http://www.jamezone.org/</a><br><br>
</div>