coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] how to file bugs against PG Coq mode?

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] how to file bugs against PG Coq mode?
Date: Thu, 15 Oct 2020 17:04:27 -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-io1-f42.google.com
Ironport-phdr: 9a23:B48lnRNJEiBNtKfckGsl6mtUPXoX/o7sNwtQ0KIMzox0I/z5rarrMEGX3/hxlliBBdydt6sbzbSN+Pm8CSQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagY75+NhS7oAveusULjoZvKbs6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyoBKjU38nzYitZogaxVoByvuQFxzY3Tbo6aKPVwcbjQfc8YSGdPQspcTTBNDp26YoASD+QBJ+FYr4zlqlcArxu+Ag+sBOLsyjBWgn/5w7M13v8uEQHDxgMgHtYOvG7Io9XyMaceX/2+wa7KzTXEafNW2DT955bMch8/v/6BRr1wcc/LxkkuEwPJlEmfqYvgPz6M0OkGrmeU4fZ6W+21l24ntx9+oiKpxso0l4TEmoIYxk7Z+Clkw4s4Jdm1RU11bNOkDZdcqjyWOpZ4TM4+QGxkpCY0x6AHtJC1YiQEyJopyhHBZ/KIfYWF7RTuX/uSLzdgnH9pZq6zihKo/UWjyuDwTNS43VdLoyZfndTAqGgB2wLS58SbV/dw+1qt1DKT2A3W5exJIFw4mbbeJpMv3LE9lp8evVrfEiPqhkn7ibOZeVsq+uim7unnbKvpqYKGOIJxlA3zPKYjlde5DO8lKAYBRXKb9v651LD7/U32XrFKjvoun6ncqp/aJMAbqre4Aw9Sz4ov8hi/Aji43NgCknkHK1VFeB2Dj4f3IV3BPPf4DfKnj1Stljdk2ezGM6X/DpnRKnXPirTscLZn50JByQc+zMpT6p1KBr0ZJfL8QE7xtNjWDh8jNAy0xv7qCNd61oMYWGKPAbGWMKfMvlCW/e8vLOyMa5UUuDb5MfQq+/nujXohlV8HYaapxYcXaGy/Hvl+P0qZZmPsjs4dHmcOowoxV/fniEaCUD5Wf3a9Rbgw5jA9CIK8DIfMXJqhgLKb3HTzIpoDbWdfT1uIDH2gI46DQrIHbD+YCs5niD0NE7a7HdwPzxar4UX4zLxmLefQ9yAwupfq1dwz7OrW31lm9ztyDseQ12yAZ25xl2IMATQx2fYs8gRG1l6f3P0g0LRjHttJ6qYRC1ZoBdvn1+V/TuvKdEfEd9aNRkyhR4z/Uz40R9M1hdQJZhQkQojwvlX4xyOvRoQtufmLCZgzqP+O2nHwI4N8zC+D2vV7yVYhRcRLOCutgastr1GPVb6MqF2QkuORTYpZxDTErT7Rwm+HvUUeWwl1A/3I

I've hit a bug in Proof General's Coq mode. To whom do I report it?

The bug is that, when "Proof using" mode -> Always is set, and one has
started a proof with "Proof with tac", this will be corrupted to "Proof
using ith tac" (w gets deleted, and using improperly inserted before
with) instead of "Proof with tac using". And, because this alteration
happens in the locked region withou undoing the proof, it can go
unnoticed until one attempts to reparse the file.

[Coq-Club] how to file bugs against PG Coq mode?, jonikelee AT gmail.com, 10/15/2020
- Re: [Coq-Club] how to file bugs against PG Coq mode?, Tej Chajed, 10/15/2020
  - Re: [Coq-Club] how to file bugs against PG Coq mode?, jonikelee AT gmail.com, 10/15/2020