<div dir="ltr"><div><span style="color:rgb(0,0,0);font-family:Helvetica;font-size:13.3333px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:nowrap;word-spacing:0px;display:inline;float:none">You can revert to b8eb5098, which is when the code was added, but before it was actually run.<br><br></span></div><span style="color:rgb(0,0,0);font-family:Helvetica;font-size:13.3333px;font-style:normal;font-variant-caps:normal;font-weight:normal;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:nowrap;word-spacing:0px;display:inline;float:none">/ Ulf<br></span></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Mar 5, 2018 at 8:23 AM, stvienna wiener <span dir="ltr"><<a href="mailto:stvienna@gmail.com" target="_blank">stvienna@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 all,<br>
<br>
My formalization doesn't work because of the open bug:<br>
<a href="https://github.com/agda/agda/issues/2888" rel="noreferrer" target="_blank">https://github.com/agda/agda/<wbr>issues/2888</a><br>
<br>
(Location of the error: Forcing.hs:230)<br>
<br>
<br>
Is there a work around so that I can keep on working?<br>
What agda commit should I revert to? (I.e., in which commit was the<br>
new forcing translation introduced?)<br>
<br>
Best,<br>
Stephan<br>
</blockquote></div><br></div>