coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?
Date: Thu, 25 Jul 2019 16:50:05 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre-marie.pedrot AT inria.fr; spf=SoftFail smtp.mailfrom=pierre-marie.pedrot AT inria.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
Autocrypt: addr=pierre-marie.pedrot AT inria.fr; prefer-encrypt=mutual; keydata= mQINBFOFpSQBEACyDotTWHydRK+7nzdk+ULrBszrG8Eu7J59+eogMOIOQYKw/joFiTOHnJgG vUzt//PqMURC7tZ72teZHeyLKHwr3a9oOC4W36Wrt4jVGvAnYk60hF20i921ljIN8aj41UYz t+8vgsqgpTCNbcgxhhgXSQ+9n/OZs1yoy6kgIE378HsIhGoGTQxmwdz2k0Aic/qun2Z4CO9v zjTjkUYMJxs4XwVsprMkO/a6qVBkNtEjbwVDJS5d7qzfph2DHJXFyUOPc1GudPI+VW2Abi4A 2US/ycyGMUTYRVaUDUF/GqfqmYgUj4vFvANdB3Roa3XDVxAlkYcNuUqtcpQi9yoU6t+Agobp nqcn+WrtOwrJtvEh3KaaQvI4Yudz3pEmP9KL2VYenUQLuDqVL4KgdCPcAZmpkSC7KCm8Ns2v y69zHasNsPD9YiIXCgpGNZEEUjrG8Si+ej3/3MTqTBQqpSzqTagtGhGANrjEgHj6zdh+plby k/bCYHjX4oDPJZQx6GjmtGPandUAD+SImEwS6WMyCKtUSKJtqD+DVNWiwKAK3+CNxDW/DbRS /N2ACdtItJhFmPAb9Nxs6O27xyPCse4n9fMCT5pLQpDfMmkOQsjr1kCWiOWgjIgfOG64HrxQ Vcjg6mf9EEGVi4kpMhl6RzZ7wsg+ff3w/5NR1e1HX9yj/UbsLwARAQABtDNQaWVycmUtTWFy aWUgUMOpZHJvdCA8cGllcnJlLW1hcmllLnBlZHJvdEBpbnJpYS5mcj6JAj4EEwECACgFAlOF pSQCGwMFCRLMAwAGCwkIBwMCBhUIAgkKCwQWAgMBAh4BAheAAAoJEHkiwB/Zujx745sP/3JA gDdlat/mjqxgpC30Jy5Rnkgblxo/qnEmmhPxSQJKt77JaaDgRfsTrJZcO1K9LN6aLs8dPo26 V29TSt0UJhw5bQcTqi/wlD/ZfQ3I69gn9x6ln3T/7TV/g0tyObbzPYQLsi6p8wgJzO1F3Dr2 9XjEfB2jVs7ancTKbE+5yvwN0v3VCrtG5cFpAdkrMtZzXbXMAxRa7HueUjtxm/ls5zqbwTZ6 1tmJlSJJS+rL43InCxDFRbPO4YzV3z7+sEw/Kpn3HwVQz6y3aDQWqQlq/vF8r0p+3E3CB+h/ h6coMySbpwHZAAMsu9KpQBqGpbAjI5RXvcNJD+7MCqT5LYy/QmULqVaLS7zaspcZc2V2CW1w 4LaZtlMjt4gedGvd/UICuy1pw1GdR3YRlUCQGKnzVp8Cw1Bsd1SbZu0DT/DOt3DHyZLliENu P6PRPQT+Rmj21mDpj+bLJliIpRWQ99/cFA6mmKv7qYk49xWsUL0YxcGabGIObBbMpFoq+Coj 8Gmm10706NrJuhYJMxdxHQNbiV8eYnC6jKnL0F3BPeEloSpw0saq/8PVU7eTwvkrOBTVfiwa UFe7HLFDo6SaRoXJAeBa22ADM4bTQCrf856BMT/4BjHdSUAj4Sq1j1QUHVTWWRVsnNH8Nz10 /n2x8sxQIf8yVX4aN/Km/uz7Xq14hL6suQINBFOFpSQBEADMsZKO9fPtbmyMlS5YQl3B+p5E 17sEJAHSNGA4rfx7Uxij1H1PnTZ0kHhngrhEG1wzv2+1aORCg31Jqrwf//XPbcv6QL4CinD7 QUpbMdrZFo296AkAjuhO8J0LvB8CY3GY6n/G3njy9ISmemEH3dAzOM87Wt0En1dcSYJxdfM2 fmWq6ghlmcQA6A6g1vJ0iKnFcvh/IXHBm1/dtVSOj+2+S4/PLALMCUzugFQLVAKiv7pkdxPz KGxMMEnQuLXjoFivXV6i3q9+0FVVo2t9LfD1EzTNoKwx4866nVnVMU9myd6IS03lKAREmHhb YRKJt+dlmJoqttVczsruFa1SRmzhpp5O2jFWzR0C+SD23s70PXaZ4wcn4TzQKL+tGMRqELLF XepqWcmKnROvX+agmeZK1UxhaIGI0JpPtZHsNGNoU1dbzUE+opzHP5Lpouc5Te+MkXe4wSM6 WrfyTRqUfVr7CeaSozkX/AfgubNnNYmi8RduUjUBjukMEsRchirbyCh1397xK90HDpiiqPy/ PLaUx/sp2vp0TSxGPFtl9CmuSOPVi0HQI51SrnckMA/zQJu6AZyFkbb7fpUi/cPds7AVCLjd mNkLOe77sZ+/D3YKXiHujrpncau+NaQ2SKMrqcRocAeogbd+VV3DFGRgHereAZwHD87ruHeg jEO92QRw/QARAQABiQIlBBgBAgAPBQJThaUkAhsMBQkSzAMAAAoJEHkiwB/Zujx7eSsQAJnw yYs/yiYjwzYdlmGQP1fuG0RG6DwHXZDti9etXRhjgOMvE4+TKqSeM9gXCxdGE7M2aKV+PJvi twb4FRLBOl9YwlHTiV5UIJpcbJv+zvdNSDrlqSSln1Qfqq7HJUvDwSKcY8316pVuF5Q9gknX P/gRG4O8e/fBXuSiL08cDudnkbhSm6zb+VGaewivO0FuuCX4RpYtF4EULbCKof7SSCK3/WWl roX6H3S6dNo/3cUGahj7FfTaQMwHH34P6wGWtJCh7vhaxQ5QdXjj8ZkJfcE03uo+GbF7/xmo g5wxtsFUWhs5G0P534BmahBBKsINIyExt6JYASYL/oouC9c+AOjc3bON7Ae1jeHgx3BSSUju 81x+5MrXAqrLhJ6xDsQpATL7qDcBEHBodo0xlAIgb71qeIU5gZUOw/43eJOnexDFs4VWMthJ z2ot6WdRzYEKt75nuCZqaaUEM+MvOGNZZRM3Dkbqw3Jik1X+lOjc/OgUs+Xn9oaIylA1nojO 9E31ulGmniydilLd+4Vd+WQn0ZEwy75EzDTl0Ne/j8nvLyzeYIWbt5/06mR2L87DIEXmXkAM mwfFXNzzX9gVX8m7owb4CPTf5DCDrguwNdvcPePy81w+fXM7c0Dq+5hzPvh5MRruEDOfqaZw HXQ4ZkGmhsCD6dMF2cKX+EqLjopA136U
Ironport-phdr: 9a23:JYPL0BfFiA5zhQXIzrB+5MRwlGMj4u6mDksu8pMizoh2WeGdxcuzYx7h7PlgxGXEQZ/co6odzbaP6eawAydfvt6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vMhm6twbcutcZjYZgKKs61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzoBOjUk8m/Yl9ZwgbpGrhy/qRxxw43abo+bO/VxfKzSYcgXRWVdUstLUCJNHo2xYosJAuEcPehYtY79p14WoBWkBAmjGvnvyiVWiXPv2qM1yf4hEQDY0wM4BdwJqmnbrM/yNKcOTOu4y7HIzTTdYPNMwzfy9pHEchU7rvGWXLJ/b9DdyVExGAzYlFWQrpDlMiiU1uQLqWib7vBvWfihi249sgx8pCWkyMQ0ioTRm44Yzl/J+T9nzIs1KtC0Uk92bcO+HJdNuSyXNJN6T80gTm1ypSo3y7ILtYSmcCQWyJkr3QPTZvKJfoWO/xntTvyeIS1ii3JgYL+/hwi98UynyuDkVcm010xKri1BktbSqHABzQHT6s6GSvtj50uhwSyA1xrS6uFfI004j6TbK4Q5zr4xkJocr1jDEzfrlEjyg6KabFso9+in5uj9Y7jqu4WQO5J6hwz9Kqgun9awAeU8MggARWib/uG82aX7/U34XrpKlOc2nbfAvJDfP8sbvK+5DBFP3oY79RmwEi2m0NMEnXQcLVJFfgiHj4nzNF3ULvD4F++zg06wnzdz2/DGIrrhD43RIXjEibftZKpy60pByAUo1t1f/JJVCrQZIP3pQEPxtdrYDgU4MwOu2ernBs99hcsiXjeEBbbcO6fPu3eJ4PguKq+Cftw7ojH4fsAk6uT0gDockEUccJ6RXJcNb2zwSuxnLl+DbD/pi80AHCESswYkS/DCiVuYUDcVaWzkDPF03S0yFI/zVdSLfYuqmrHUhH7nTK0TXXhPDxW3KVmtb5+NAq9eaSSII8YnnCZWDeH8Gb9k7gmnsUrB85QiLufQ/XdE55Hkzt9x6vOViBcz63lsBt6cyD7LQXsmxjpZFQ9z57h2pAlG8nnG1KF5h/JCEtkKv6FIVB07PNjS1b4hBg==
Openpgp: preference=signencrypt

Hello Michael,

On 25/07/2019 14:35, Soegtrop, Michael wrote:
> I wanted to write a simple tactic in Ltac2 to cbn just a given part of
> the goal, but I don’t understand how I can pass on a ltac2 variable to a
> call to a ltac2 notation.

After a quick look at it, it is actually a defect of the pattern scope,
which doesn't seem to properly handle term antiquotations.
Interestingly, I don't remember if I didn't implement that on purpose,
because the ability to inject arbitrary terms into patterns rely on the
dreaded pattern_of_constr function whose semantics is flaky, to say the
least.

Anyways, it should be easy to fix, hopefully. I'll submit a PR soon.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?, Soegtrop, Michael, 07/25/2019
- Re: [Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?, Pierre-Marie Pédrot, 07/25/2019
  - RE: [Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?, Soegtrop, Michael, 07/26/2019