<div dir="ltr"><div>This is indeed fixed in the development version: see <a href="http://code.google.com/p/agda/issues/detail?id=920">http://code.google.com/p/agda/issues/detail?id=920</a>.<br><br></div>Jesper<br></div><div class="gmail_extra">
<br><br><div class="gmail_quote">On Thu, Dec 19, 2013 at 12:00 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div class="im"><br>
<br>
On 19/12/13 10:37, Ulf Norell wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
It looks like this has been fixed. In the development version I get<br>
yellow on all variants of the example.<br>
</blockquote>
<br></div>
Great. Fortunately I don't use "_" often in proofs. But I worry that<br>
the one or two occasions in which I did may be unfillable!<br>
<br>
I shall try the development version.<br>
<br>
Thanks,<div class="HOEnZb"><div class="h5"><br>
Martin<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</div></div></blockquote></div><br></div>