Opened 14 years ago

Closed 14 years ago

#359 closed defect (fixed)

Fix coq.el bindings (coq-insert-term, proof-store-goals-win, & coq-SearchAbout)

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

Description

I suggest to fix 3 key bindings issues in coq/coq.el:

The correct binding triggered by the keystroke "C-SPC" is [(control ?\s)], whereas the old one prevented from calling coq-insert-term.

For a similar reason to #341, we should avoid to bind a key that involves a "C-g" (suffix or whatever), which was the case for proof-store-goals-win; the same shortcut with capital G is free.

And for coq-goals-mode-map, coq-SearchAbout shouldn't be lowercase.

Kind regards, Erik Martin-Dorel.

Attachments (1)

coq-el.patch​ (2.1 KB) - added by Erik Martin-Dorel 14 years ago.
Patch for coq/coq.el

Download all attachments as: .zip

Change History (2)

Changed 14 years ago by Erik Martin-Dorel

Attachment: coq-el.patch​ added

Patch for coq/coq.el

comment:1 Changed 14 years ago by David Aspinall

Resolution: → fixed
Status: new → closed

Applied patch, many thanks!

Note: See TracTickets for help on using tickets.