coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] specialize a subset of the parameters of a hypothesis

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] specialize a subset of the parameters of a hypothesis
Date: Wed, 13 Jan 2016 11:00:01 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm0-f43.google.com
Ironport-phdr: 9a23:zKy1yB8H1gSMbv9uRHKM819IXTAuvvDOBiVQ1KB91O0cTK2v8tzYMVDF4r011RmSDdudu60P07eempujcFJDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXsq3G/pQQfBg/4fVIsYL+lRMiC0I/viqibwN76XUZhvHKFe7R8LRG7/036l/I9ps9cEJs30QbDuXBSeu5blitCLFOXmAvgtI/rpMYwuwwZgf8q9tZBXKPmZOx4COUAVHV1e1wysebsrFHoSRaFri8XVXxTmR5VCSDE6gv7V9H/qH2pmPB63XyiPMDsV718cjO/9btqRQKg3D8GOiQj/SfcjdFqkKNWvTquohV+x8jfZ4TDZ6k2Rb/UYd5PHTkJZc1WTSEUR9rkN4Y=

Works great, thanks!
P.

2016-01-12 17:12 GMT+01:00 Jonathan Leivent
<jonikelee AT gmail.com>:
>
>
> On 01/11/2016 11:28 AM, Jonathan Leivent wrote:
>>
>>
>>
>> On 01/11/2016 05:35 AM, Pierre Courtieu wrote:
>>>
>>> Nice, thanks Jonathan!
>>>
>>> One small glitch yet: the name of the re-asbtracted hypothesis are not
>>> kept
>>> the same. I guess it is hard to keep them around.
>>>
>>> P.
>>
>> Unfortunately, I don't think there's a way to keep the names and also get
>> the generality and fairly nice syntax, because of limitations of Ltac.
>>
>
> I lied.
>
> Here is a version with a very slightly less nice syntax (a prefix operator),
> but that keeps the names. It also no longer needs to use number_goals.
> Examples are at the end of the attached file.
>
> -- Jonathan
>

Re: [Coq-Club] specialize a subset of the parameters of a hypothesis, Pierre Courtieu, 01/08/2016
- Re: [Coq-Club] specialize a subset of the parameters of a hypothesis, Jonathan Leivent, 01/08/2016
  - Re: [Coq-Club] specialize a subset of the parameters of a hypothesis, Pierre Courtieu, 01/09/2016
    - Re: [Coq-Club] specialize a subset of the parameters of a hypothesis, Jonathan Leivent, 01/09/2016
      - Re: [Coq-Club] specialize a subset of the parameters of a hypothesis, Pierre Courtieu, 01/11/2016
        
        Re: [Coq-Club] specialize a subset of the parameters of a hypothesis, Jonathan Leivent, 01/11/2016
        
        Re: [Coq-Club] specialize a subset of the parameters of a hypothesis, Jonathan Leivent, 01/12/2016
        
        Re: [Coq-Club] specialize a subset of the parameters of a hypothesis, Pierre Courtieu, 01/13/2016