<div dir="ltr">In agda-mode, when displaying values imported from modules with parameters, they are displayed as, e.g.<div><br></div><div>    .#Context-110877108.[]<br></div><div><br></div><div>In addition, when using automatic rewriting, such as automatic casing (C-c C-c) the patterns are written as such.</div>

<div><br></div><div>Is there any way to avoid this, and have agda-mode use the simple imported name</div><div><br></div><div>     []</div><div><br></div><div>instead?</div><div><br></div><div>Pepijn</div></div>