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

[Wojciech Jedynak]

Hello everybody!

I don't know if anybody actually tried running it (;-) ), but I
noticed a big mistake with respect to emacs key binding in the elisp
code I announced last night.
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).

To apply the fix in the agda2-mode-el file change
 (agda2-solve-with-db "\C-u\C-c\C-a" (local) "Auto with theorems from
the given db (or global if none given)")

to
 (agda2-solve-with-db "\C-c\C-v" (local) "Auto with theorems from the
given db (or global if none given)")

The fixed code and updated tutorial are available at
https://github.com/wjzz/Agda-mode-improvements

Again, pardon the noise, I'll be less verbose in the future :-)

Greetings,
Wojciech Jedynak