[Agda] ANN: agda-move-improvements-0.3

[Nils Anders Danielsson]

On 2011-06-12 12:28, Wojciech Jedynak wrote:
> This is a follow-up to those ANNs:
> * ANN: coq-like agda-mode support for databases of lemmas
> (http://article.gmane.org/gmane.comp.lang.agda/2911)
> * ANN: convenient way to add a with expression from a goal
> (http://article.gmane.org/gmane.comp.lang.agda/2928)

One minor point: We try to avoid making the Emacs mode too complicated,
preferring it to be a thin layer over the Haskell backend. Hence it is
unlikely that we will include your functions in the "default" Emacs
mode, should you want that. You can of course distribute your additions
separately, as you do now.

-- 
/NAD