<div dir="ltr">Our emails crossed--I had found this as well.<div><br></div><div>Unfortunately I don't recall just which version I was using prior to 2.5.1; I thought it was the most recent 2.4.x but I may well be wrong, and I'm not sure how I can reconstruct that information. Perhaps it doesn't matter anyway as long as the 2.5.1 behavior is clearly specified.</div><div><br></div><div>Thanks very much Andrés and Andrea for your help. Incidentally Andrea you may not remember but we met and talked at OPLSS last year--you were very helpful then as well!</div><div><br></div><div>John</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Feb 16, 2016 at 5:13 AM, Andrés Sicard-Ramírez <span dir="ltr"><<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 16 February 2016 at 08:03, John Leo <<a href="mailto:leo@halfaya.org">leo@halfaya.org</a>> wrote:<br>
> Thanks for the pointer to C-u C-u; that is indeed useful.<br>
<br>
</span>From the CHANGELOG, it was introduced in Agda <a href="http://2.4.0.1" rel="noreferrer" target="_blank">2.4.0.1</a>:<br>
<br>
* Key bindings for controlling simplification/normalisation:<br>
<br>
Commands like "Goal type and context" (C-c C-,) could previously be<br>
invoked in two ways. By default the output was normalised, but if a<br>
prefix argument was used (for instance via C-u C-c C-,), then no<br>
explicit normalisation was performed. Now there are three options:<br>
<br>
* By default (C-c C-,) the output is simplified.<br>
<br>
* If C-u is used exactly once (C-u C-c C-,), then the result is<br>
neither (explicitly) normalised nor simplified.<br>
<br>
* If C-u is used twice (C-u C-u C-c C-,), then the result is<br>
normalised.<br>
<span class=""><br>
<br>
> It's still<br>
> curious that 2.5.1 seems to be evaluating one fewer step by default than 2.4<br>
> did;<br>
<br>
</span>There are various 2.4.* versions. Which version you are talking about?<br>
<span class="HOEnZb"><font color="#888888"><br>
<br>
--<br>
Andrés<br>
</font></span></blockquote></div><br></div>