<div dir="ltr"><div><div>As Andrés said, I unfortunately cannot test DoCon-A-0.03 with my new unifier because I get a parse error at source/Int/Integer1.agda:418,11-422,15. Do you have a version that is compatible with the current Agda master?<br><br></div>regards,<br></div>Jesper<br><div><div><div><div><br></div></div></div></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Dec 15, 2015 at 2:32 PM, Andrés Sicard-Ramírez <span dir="ltr">&lt;<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><span class="">On 14 December 2015 at 16:10, Sergei Meshveliani &lt;<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>&gt; wrote:<br>
&gt; You can use the test of  DoCon-A-0.03:<br>
&gt;<br>
&gt; <a href="http://www.botik.ru/pub/local/Mechveliani/docon-A/0.03/" rel="noreferrer" target="_blank">http://www.botik.ru/pub/local/Mechveliani/docon-A/0.03/</a><br>
<br>
</span>DoCon-A-0.03 doesn&#39;t type-check with the development version (i.e. the<br>
master branch), so it&#39;s not possible to test Jesper&#39;s new unifier.<br>
<span class=""><br>
&gt;<br>
&gt; I am not sure that I would try it now, because it is very difficult to<br>
&gt; advance the project when trying different tool versions.<br>
&gt;<br>
<br>
</span>It&#39;s not difficult to test Jesper&#39;s new unifier. By running<br>
<span class=""><br>
  $ git clone <a href="https://github.com/jespercockx/agda.git" rel="noreferrer" target="_blank">https://github.com/jespercockx/agda.git</a> agda-unification<br>
  $ cd agda-unification<br>
  $ git checkout --track  origin/unification<br>
  $ make install-bin<br>
<br>
</span>you get a version of Agda including Jesper&#39; new unifier (Agda 2.5).<br>
After type-checking you code, you remove the agda-unification<br>
directory and you re-install Agda from your current directory.<br>
<span class="HOEnZb"><font color="#888888"><br>
<br>
--<br>
Andrés<br>
</font></span></blockquote></div><br></div>