[Agda] include directories and agda-mode "warping" between files

[Nils Anders Danielsson]

On Tue, Jul 15, 2008 at 4:08 PM, WILSON F.A.J.
<frank.wilson at durham.ac.uk> wrote:
>
> It seems that if you purge the library directory _as well as_ your work
> directory of agdai/agda.el files then warping should start working again.

The agdai files contain the range (absolute path of file + position in
file) of every identifier defined in the module. So yes, if you move
the files you need to retypecheck them. If we had a package system
(like GHC) we could use relative paths instead of absolute ones, and
then you would not have this problem.

-- 
/NAD