coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac2 retraction bug?

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Ltac2 retraction bug?
Date: Thu, 23 Apr 2020 00:57:08 +0200
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-il1-f179.google.com
Ironport-phdr: 9a23:PthzrRcMLuBFqf4mIGM+SinwlGMj4u6mDksu8pMizoh2WeGdxcS5Zh7h7PlgxGXEQZ/co6odzbaP7ua8CSdZu96oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLBi6twrcu8oZjYd/NKo61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzocOjUn7G/YlNB/jKNDoBKguRN/xZLUYJqIP/Z6Z6/RYM8WSXZEUstXSidPAJ6zb5EXAuUOM+ZXrYnzqVUNoxWjGwejGPjixSVUinLsx6A2z/gtHAPA0Qc9H9wOqnPUrNDtOakIUOC60rPIzS/dYPhLxzr975XIcgo9ofGNQ71wbNfaxE43FwPEkFqQs5blMC2P2usRtGib8vBgVf6ui2E5tgF8uTevxsI2hYnIgoIZ0EzL9SJ8wIssI9CzVUB1YdmhEJRKtiGaMZN7QswjQ2F0uCY616YJtYSncygNzZQqwQPUZf+fc4WQ/B7vSOKcLS17iX9lYr6zmhe//Em6xuHhVMS51FBHpTdfnNbWrHACzRnT59CHSvRj+keh3i6C1wXJ5eFFJUA4jKvbK5o8zrIpmJofrEbOEyvslEX5i6+WcUok+uy25Oj9frrmoZqcO5d1igH4LKsuhtSyDfokPgUKRWSW+uSx2Kf+8UD4QbhGlOA6n6vdvZzCIMQUvK+5Awtb0oY57Ba/Ci+r0MwZnXYZNlJFYgyIg5L1NFHJPfD4F+u/g1Wynzd23P3GMbjhDY/MLnjHirvuYbF960tExAop0d9f/45UCq0GIP/rRkDxs8XYAgYlPAyw3uboE85w1pgeWGKKGq+WKrnesV6O5uI1IumDfpUZuDjnK6tt2/m7pngg0XQZYKPhiZAQcTWzGulsC0Sfe3vlxNkbRzQkpA07GdTrhUeYXHZ4YGuoQ6Mx+3lvEIOrF53OAIuqnaad3SqmNpJTb2FCTFuLFCG7JM2/R/4QZXfKcYdamTseWO3kEtd5jE38hErB07Nia9Hs1GgAr5u6jYp64uTSkVc58jkmV53AgVHIdHl9myYzfxFz3K17phYjmFKK0Kw9gvgBUNIKuKIPXQA9OprRied9DoKqA1OTTpKyUF+jB+6eL3Q0R9M1zcUJZh8kSdqnhxHHmSGtBu1Mmg==

I can also reproduce it with coqide.

I think you should fill a bug report on coq github page please?: https://github.com/coq/coq/issues

Regards,

Pierre

Le mer. 22 avr. 2020 à 23:03, Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de> a écrit :

Hi,

On 22/04/2020 22:36, jonikelee AT gmail.com wrote:
> I'm using Coq 8.11.0. Could someone verify that this isn't only me
> doing something stupid?

I can reproduce the bug. (Coq version 8.11.1)

[Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, Jason Gross, 04/22/2020
  - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
    - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
- Re: [Coq-Club] any Ltac2 examples out there?, Tej Chajed, 04/22/2020
  - Re: [Coq-Club] any Ltac2 examples out there?, jonikelee AT gmail.com, 04/22/2020
  - [Coq-Club] Ltac2 retraction bug?, jonikelee AT gmail.com, 04/22/2020
    - Re: [Coq-Club] Ltac2 retraction bug?, Maximilian Wuttke, 04/22/2020
      - Re: [Coq-Club] Ltac2 retraction bug?, Pierre Courtieu, 04/23/2020
        
        Re: [Coq-Club] Ltac2 retraction bug?, jonikelee AT gmail.com, 04/23/2020