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: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Ltac2: how to use ltac2 constr variables in calls to ltac 2 notations?
Date: Fri, 26 Jul 2019 09:13:14 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga04.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.600.7
Ironport-phdr: 9a23:nrrdthYOEoJ/i2n8AGTFEc3/LSx+4OfEezUN459isYplN5qZr8m/bnLW6fgltlLVR4KTs6sC17OM9fC8EjVaqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba5sIBmsrgjcucYajZZ8Jq0s1hbHv3xEdvhMy2h1P1yThRH85smx/J5n7Stdvu8q+tBDX6vnYak2VKRUAzs6PW874s3rrgTDQhCU5nQASGUWkwFHDBbD4RrnQ5r+qCr6tu562CmHIc37SK0/VDq+46t3ThLjlSEKPCM7/m7KkMx9lKJVrgy8qRxjzYDaY4+VO/h/fqzBctwUSnFMXtpIVyFFHo+wc5cDA/QHMO1Fr4f9vVwOrR6mCAWiGe3vzSFHhnDq3a0g1OQhCRnK1xEnEdIPrHvUrM/6O7kWUey70aLFyjDDb/JK1jf98ofHbBQhreuXXbJ3b8XRxlUvFxnCjlWIsoHlPjWV1vgTvGif9eZvSeWvi2s+pgx3vzOhyMAsiozTiYIUzFDJ7SR5wIApJdKmTE53e8OrH4VWuiqHNIV2WtsvT3xstSok0LELuZ62cDIKxZg53RLTduKLf5SQ7h7+VeucLy10iXxrdb6lmRq//0ytxvfhWsS3zVpGtjdJn9jIu3wXyRDe6seKRuFj8ku72TuC0wbe4fxeL08uj6rUMZshz6YwlpUNtUTDGTf7mED5jKCMakkp9fKk6+XhYrX6uJCcM5V4hR35MqQrgsC/AOI4PRYSX2WD5Oix0KPv8Vf5TbhKlPE7krfVvIrHKcgFuqK1GwpV3Zwi6xa7ATemytMYnXwfIVJAeRKIk4jpNEvQL/D8F/u/mFOsnylkx/DaJL3hBY3NI2PCkLfnYbZy9UpcxBAvwtBY4pJYEqsBL+7rWk/tqNzYCQc0PBCzw+b+EdlyyoceWX+UDaKCK6PTsVqI5vo1LOWWZY8Vviz9K/k/6PL0g385gwxVQa78l5AQcTWzGulsC0Sfe3vlxNkbWy9etQ0nCefulVeqUDhJZn/0UbhqtR8hD4fzR7zES4+xmruZmG+eH5ZWb21CQBjYFHbjd4yJX7EXby+dPtVmihQFU6SsT8kq0hT451yy8KZuMueBon5QjpnkztUgv7SOxyF3ziR9CoGm60/IT2xwmTpXFTo51fgj50171lqHl6N/hq4ATIAB17ZySg4/cKXk4aliEdmrA1DAeMuETBCtRdD0WWhgHOJ0+McHZgNGI/vnixnC2ySwBLpMzu6KAoA59uTX2H2jfss=

Dear Pierre-Marie,

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

Interesting that this is a non-trivial problem.

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

Thanks - I am looking forward to it!

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Gary Kershaw
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[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