coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Context menu in Proof General

From: "Paul A. Steckler" <steck AT stecksoft.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] Context menu in Proof General
Date: Fri, 24 Feb 2017 16:57:51 -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-ua0-f172.google.com
Ironport-phdr: 9a23:4YUy6RKwm+oS+nxX69mcpTZWNBhigK39O0sv0rFitYgXIvTxwZ3uMQTl6Ol3ixeRBMOAuq8C0bKd6v2+ESxYuNDa7yBEKMQNHzY+yuwo3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEtfre9ScbuiJG80Pn38JnOaU0cjz2kJLh2MR+erAPLt8BQj5E0eYgrzR6c6ENBZuAe7CUgHk6elBX46936tMp47ylbuNo668NLUr79cbh+RrtdWmd1e1sp7dHm4EGQBTCE4WERBz0b

In Proof General, do you use the Show/Hide context menu? If so, do you
use it to hide individual items, like tactic calls, or Notation
declarations, or do you use to hide chunks, like proofs and sections?

I'm working on a new version of Proof General, and I can get some
speedup if I can avoid creating some of those context menus, so I'd
like to get some sense of how this feature is used.

-- Paul

[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