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 15:04:23 -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-qt0-f195.google.com
Ironport-phdr: 9a23:SxAU5hQv4qc0TTUhhklV2RefYdpsv+yvbD5Q0YIujvd0So/mwa64ZxGN2/xhgRfzUJnB7Loc0qyN4vimBzFLuMzd+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLshrj0pcCYOl8UzBOGIppKZC2sqgvQssREyaBDEY0WjiXzn31TZu5NznlpL1/A1zz158O34YIxu38I46FppIZ8VvDxeL19RrhFBhwnNXo07Yvlr0rtVwyKs1kbVGwKkhNOSyzI7Q/3WIu55in9sOt+1S2XMOX5SLk1XXKp6KI9G0ygszsOKzNsqDKfscd3lq8O+B8=

On 07/27/2016 02:59 PM, Matthieu Sozeau wrote:

.. Maybe a
modifier like unshelve would be more suited.

+1

-- Jonathan

Re: [Coq-Club] Apply without TC inference, (continued)
- 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