coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac2 retraction bug?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Pierre Courtieu <pierre.courtieu AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ltac2 retraction bug?
Date: Wed, 22 Apr 2020 19:17:40 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qv1-f46.google.com
Ironport-phdr: 9a23:1EaSeRVtrAn7KgfIFpt5SktKgSvV8LGtZVwlr6E/grcLSJyIuqrYbRSOt8tkgFKBZ4jH8fUM07OQ7/m9HzBQqs/f+Fk5M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi2oAnLucQbgoRuJrswxxDUvnZGZuNayH9yK1mOhRj8/MCw/JBi8yRUpf0s8tNLXLv5caolU7FWFSwqPG8p6sLlsxnDVhaP6WAHUmoKiBpIAhPK4w/8U5zsryb1rOt92C2dPc3rUbA5XCmp4ql3RBP0jioMKiU0+3/LhMNukK1boQqhpx1hzI7SfIGVL+d1cqfEcd8HWWZNQsNdWipcCY2+coQPFfIMM+hYoYfjulUArhmxBQerCuzg1jBGiWT73bE43uk7DQ3LxhAsE8wIvX/JrNv1LqASUeWtwaXGzzXDaPVW2Tb+6IfWdhAuv++DUKl/ccrU00YvFgfFgk+MpoziOjOZ2PkGvm+Z7+pnU+Kvim0npB91ojex2MghkYbJhocPxVDF8SV12po6Jdq9SENiZ9OvDZVetyafN4RsQ8MiRXlluCk7yr0auZ67YTMFxI47yB7YbvyKdZWD7BH7VOuJPzt0mHZodKi8ihuy60Ss1PDwW82u3FtFrydJisfAu3ER2xDO78WLV/9w8Vuk1DuA1g3f9v1ILEUpmqfbMZEsx6M/m5kIvkvdGyL7l175jKGYdkgh9Oin9eXqbavjq5KYK4B4lBzxP6IzkcKlG+s4KBIBX22D9OS8yrLj+Ur5Ta1PjvIsk6nZtInWJd0FpqKkGgNV3Iku5helAzep19QYmnYHLFZbdx6dk4fpPFTOLOj5Dfe5nVusjC9my+7aMrDlGJnALXjOnK3/cbpg70NQ0gU+wNFH65JREL4BIfbzWkHrtNzfCx80Kw60w+HhCNV81YMRR2aPDbGHP67Jvl+I4/ggI+iIZIMPpDn9LP0l6+b0jXAlgV8dYbWp3ZwPZX+kGfRmOlyVbmbogtccCmgHpRE+TezviF2aSzFffXeyX6Qm5jE6Eo2qF4nDRpr+yICGiR+6E4dMayhtDU2WDXblas3QQ/YBcjifZMRmjyYYVLW8Y4Ak3BCq8gT9zuw0APDT/3hSt5Xl1dt44+DevR43/D1wSc+a1ivFG2NzmGILSjs70YhwpEV8zhGI1q0u0K8QLsBa+/4cClRyDpXb1eEvTomqAluQLOfMc06vR5CdOR90S9swx9EUZEMkQoetixnC22yhBLpHzuXWVqxxybrV2j3KH+g4y3vC0/N83VwvQ88KLHP/w6AjqU7cAInGl0jfnKGvJ/xFgHz9sVybxG/Lh3l2FRZqWPycD38ab0rS69/+4xGaQg==

On Thu, 23 Apr 2020 00:57:08 +0200
Pierre Courtieu
<pierre.courtieu AT gmail.com>
wrote:

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

Kenji Maillard told me in a private email it is this already-reported
bug: https://github.com/coq/coq/issues/11793

[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