coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Jonathan Leivent <jonikelee AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Apply without TC inference
Date: Wed, 27 Jul 2016 12:09:36 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f175.google.com
Ironport-phdr: 9a23:AoiULx8bAkAgef9uRHKM819IXTAuvvDOBiVQ1KB91+0cTK2v8tzYMVDF4r011RmSDN2dta8P2rKempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47AblHf6ke/8SQVUk2mc1EkfqKrR8WD14ye7KObw9XreQJGhT6wM/tZDS6dikHvjPQQmpZoMa0ryxHE8TNicuVSwn50dxrIx06vrvGZp8E4tnwM87J8r48TGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JcGIQmwZICg6NyBz7QJr3rmOutO172SqXOcD7Zb8xUDWmqaxsTUm72288Kzcl/TSP2YRLh6VBrUf8/xE=

On 07/27/2016 11:59 AM, Jason Gross wrote:

https://coq.inria.fr/bugs/show_bug.cgi?id=3841 ,
https://coq.inria.fr/bugs/show_bug.cgi?id=3495

Those both appear to be fixed in 8.5pl2. Fortunately.

-- Jonathan

[Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
  - Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
    - Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
      - Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
        
        Re: [Coq-Club] Apply without TC inference, Jason Gross, 07/27/2016
        
        Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
    - Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
- Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
  - Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
    - Re: [Coq-Club] Apply without TC inference, Matthieu Sozeau, 07/27/2016
      - Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016
        
        Re: [Coq-Club] Apply without TC inference, Robbert Krebbers, 07/27/2016
        
        Re: [Coq-Club] Apply without TC inference, Clément Pit--Claudel, 07/27/2016
        
        Re: [Coq-Club] Apply without TC inference, Jonathan Leivent, 07/27/2016