coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?
Date: Thu, 28 Jun 2018 10:09:28 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT juno.mpi-klsb.mpg.de
Ironport-phdr: 9a23:DLYcRh+ioHvNZf9uRHKM819IXTAuvvDOBiVQ1KB52+wcTK2v8tzYMVDF4r011RmVBduds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55zebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRgL2hicJNzA382/ZhcJ/g61ZvB2vqAdyw5LXbYyPKPZyYq3QcNEcSGFcXshRTStBAoakYoUTFeUBOehYpJT5qVsTqxu+ChSnCeTtyj9VgH/20rY30+E5EQHHxQAgBNwPsG/OoNXyLqcSXvm4wa/VxjvAd/NbwSrx5YbMfxw7vP2BWah8fMnQxEU1GA7Jkk2cpZHrMj6RzOgBrmyW4/B9We+uiGMrsQN8rzupy8wxkIfGnJgVxUrB9ShhwIY6O9m4SEljbN6mDZtQsSaaO5FzQsM6QmFkoSU6yrkduZGgZiQKzYwnxxHFZ/OabYeE+hPjVOCPLjdknH9pZbyyihKo/US9zuDwTMq53VdQoidKjtXArnUN2AbS6siDRPt95ECh2TOX2gDR9+FEJ080mLHeK545w748j4ETsErYHiPsn0X2lqCWel0++ue08+TnfqnmppiEOoBojQH+K70ildC7AeQlKQcDRHOb+OS51L3750L1WrRKjvsskqnYqp/WP8obprTqSzNSh40k8lO0Cyqs+NUeh3gOalxfKzydiI28AVjKLrjaEPGwywCujTFk7/XeP/j6HY6LKWLMxuSyNY1h4lJRnVJghetU4IhZX+lYcaDDH3TpvdmdNScXdgm9wuLpEtJ4j9hMXHqOR7SGK+XVq1Dav7tzcdnJX5ccvXPGE9Zg/+Tn1CRrnEccOLK2xt0Qcn/qRq07cXXcWmLlh5I6KUlPvgc6S7aw2l+fVzkVYm6zGqE4/Tt9DZqpS4vOFNig

Hi,

On 28.06.2018 09:41, Yannick Forster wrote:
>   Goal exists (n : nat), n = 2.
>     eexists.
>     instantiate (1 := ltac:(refine (S _))).

Ah, right, I forgot to add the `ltac:`. What Yannick wrote is what I meant.
My
proposal probably parsed as the completely wrong thing.

; Ralf

[Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, John Grosen, 06/27/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Jason -Zhong Sheng- Hu, 06/27/2018
  - RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, John M Grosen, 06/27/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Ralf Jung, 06/28/2018
  - Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Yannick Forster, 06/28/2018
    - Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Ralf Jung, 06/28/2018
      - RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Soegtrop, Michael, 06/28/2018
        
        Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Ralf Jung, 06/28/2018
        
        RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, John M Grosen, 06/29/2018
        
        RE: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Soegtrop, Michael, 06/30/2018
        
        Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Armaël Guéneau, 06/30/2018
    - Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Gaëtan Gilbert, 06/28/2018
- Re: [Coq-Club] Is it possible to perform tactics in an existential's context from Ltac?, Robbert Krebbers, 06/28/2018