Opened 14 years ago

Closed 13 years ago

#357 closed enhancement (fixed)

Feature suggestion: function + binding to insert Coq closing tactics

Reported by: Erik Martin-Dorel Owned by: David Aspinall
Priority: major Milestone: PG-Emacs-4.1
Component: 7:prover-coq Keywords:
Cc: Erik Martin-Dorel

Description

I have noticed that Coq closing tactics are defined in coq-syntax.el, wisely separated from the others tactics, but not available for insertion.

It would be convenient, for example, to have a function coq-insert-solve-tactic similar to coq-insert-tactic, which would help the user to insert one of these closing tactics.

As [C-c C-a C-c] and [C-c C-a C-s] are already used, I would suggest to bind this new function to something like [C-c C-a !] which is probably easier to remember.

Kind regards, Erik Martin-Dorel.

Attachments (1)

coq-insert-solve-tactic.diff (1.4 KB) - added by Erik Martin-Dorel 14 years ago.
Patch for coq/coq.el

Download all attachments as: .zip

Change History (4)

comment:1 Changed 14 years ago by David Aspinall

Erik, would you care to upload a patch for this one too? It sounds like it would be a useful improvement.

comment:2 Changed 14 years ago by David Aspinall

Milestone: PG-Emacs-4.0PG-Emacs-4.1

Moving to next version (unless patch comes soon!)

Changed 14 years ago by Erik Martin-Dorel

Patch for coq/coq.el

comment:3 Changed 13 years ago by David Aspinall

Resolution: fixed
Status: newclosed

Patch applied, many thanks!

Note: See TracTickets for help on using tickets.