[Agda] ANN: coq-like agda-mode support for databases of lemmas - important bugfix

[Nils Anders Danielsson]

On 2011-05-28 01:06, Wojciech Jedynak wrote:
> Since having the new command in scope breaks the behavior of all
> commands that start with C-u (like 'C-u C-x =') I'm taking the liberty
> to write about it here. In the fixed version the agda2-solve-with-db
> command is invoked with C-c C-v instead of C-u C-x C-a (now I learned
> how bind it correctly, but the new binding seems much better anyway).

The Emacs Lisp Reference Manual contains some conventions for major mode
key bindings:

   http://www.gnu.org/software/emacs/elisp/html_node/Major-Mode-Conventions.html

Your new binding follows these conventions.

-- 
/NAD