coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Context menu in Proof General

From: "Paul A. Steckler" <steck AT stecksoft.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Context menu in Proof General
Date: Mon, 27 Feb 2017 12:10:07 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=stecksoft AT gmail.com; spf=Pass smtp.mailfrom=stecksoft AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr0-f170.google.com
Ironport-phdr: 9a23:AEodwR+o0t96Kv9uRHKM819IXTAuvvDOBiVQ1KB+2+0cTK2v8tzYMVDF4r011RmSDNidsawP2ree8/i5HzdfsdDZ6DFKWacPfiFGoP1epxYnDs+BBB+zB9/RRAt+Iv5/UkR49WqwK0lfFZW2TVTTpnqv8WxaQU2nZkImbtjyT4XVloG80/24s8nYZBwNjz6ga5tzKg+3pEPfrJ9Fr5FlL/N78hLUpjNhPaxt2W5jJlaehVy0stys8ZVg2z9Mtvki7MlOTePxeKFuHu8QNygvL21gvJ6jjhLEVwbavnY=

On Sat, Feb 25, 2017 at 4:48 AM, Théo Zimmermann
<theo.zimmi AT gmail.com>
wrote:
> Not only I don't use it but I sometimes get bitten by it (inadvertently
> calling Hide through some keyboard shortcut).
> The only Show/Hide facility that I use is the one provided by Company-Coq.

Given that there's a similar facility in company-coq, I'm tempted to
remove the feature from PG/xml.

Although only a handful have responded to my query, I certainly
haven't seen enthusiastic support for the feature.

[Coq-Club] Context menu in Proof General, Paul A. Steckler, 02/24/2017
- Re: [Coq-Club] Context menu in Proof General, Théo Zimmermann, 02/25/2017
  - Re: [Coq-Club] Context menu in Proof General, Paul A. Steckler, 02/27/2017