coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Apply without TC inference

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 14:37:54 -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-f169.google.com
Ironport-phdr: 9a23:uz9bPh9TsCitbf9uRHKM819IXTAuvvDOBiVQ1KB90O8cTK2v8tzYMVDF4r011RmSDN2dta8P0rCP+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2WVTerzWI4CIIHV2nbEwud7yzRNOZ1p7un8mJuLTrKz1SgzS8Zb4gZD6Xli728vcsvI15N6wqwQHIqHYbM85fxGdvOE7B102kvpT4r9Zf9HFbvOtk/MpdW437eb45RPpWFmcIKWcwse/ssxDfTQKJrl8RU3sblAYAVwrC6hD5U5P8vwP1s+N83G+ROsigHuN8Yiir86o+EEygsywALTNsqGw=

On 07/27/2016 09:35 AM, Jonathan Leivent wrote:

... But, I didn't know about class_apply ....

Note that class_apply defined in Classes.Init, based on another undocumented tactic autoapply. If the comments are to be believed, the intention is merely to have an apply that respects the Transparent/Opaque hints in the db it is given. So, it may be the case that this behavior of class_apply that has it not inducing inference in subgoals is an unintended side-effect.

-- 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