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)
Change History (4)
comment:1 Changed 14 years ago by
comment:2 Changed 14 years ago by
Milestone: | PG-Emacs-4.0 → PG-Emacs-4.1 |
---|
Moving to next version (unless patch comes soon!)
comment:3 Changed 13 years ago by
Resolution: | → fixed |
---|---|
Status: | new → closed |
Patch applied, many thanks!
Note: See
TracTickets for help on using
tickets.
Erik, would you care to upload a patch for this one too? It sounds like it would be a useful improvement.