<div dir="ltr">Yes, it seems to be this issue. Thanks for the link! :)</div><div class="gmail_extra"><br><br><div class="gmail_quote">On 21 August 2014 13:38, Andrea Vezzosi <span dir="ltr"><<a href="mailto:sanzhiyan@gmail.com" target="_blank">sanzhiyan@gmail.com</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
Does it happen only for constructors? If so it seems to be this bug:<br>
<br>
<a href="https://code.google.com/p/agda/issues/detail?id=896" target="_blank">https://code.google.com/p/agda/issues/detail?id=896</a><br>
<br>
Cheers,<br>
Andrea<br>
<div><div class="h5"><br>
<br>
On Thu, Aug 21, 2014 at 12:05 PM, Pepijn Kokke <<a href="mailto:pepijn.kokke@gmail.com">pepijn.kokke@gmail.com</a>> wrote:<br>
> In agda-mode, when displaying values imported from modules with parameters,<br>
> they are displayed as, e.g.<br>
><br>
> .#Context-110877108.[]<br>
><br>
> In addition, when using automatic rewriting, such as automatic casing (C-c<br>
> C-c) the patterns are written as such.<br>
><br>
> Is there any way to avoid this, and have agda-mode use the simple imported<br>
> name<br>
><br>
> []<br>
><br>
> instead?<br>
><br>
> Pepijn<br>
><br>
</div></div>> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
</blockquote></div><br></div>