Nils Anders Danielsson

I wonder if a variant of issue #6429 affects `--polarity`. Is the following code accepted? ```agda {-# OPTIONS --polarity #-} postulate @++ _ : Set @- _ : Set →...

Is anyone using `POLARITY` pragmas for anything? I don't think I'm using them.

> Regarding the name of the library file, it might make sense to have a canonical name for the project file so we don't have the issue with having to...

I reopened this PR by accident.

The changes that have been pushed are not documented in the changelog.

> * [ ] regarding its status as a contribution to the library, would a compromise (sensible/defensible or otherwise) be to suggest that it move, wholesale, to the `README` hierarchy...

I think we can close this in favour of #6582.

> but I have to better understand why the variable is being used in the first place to decide if this is also acceptable: If the buffer is modified, then...

Currently there are 67 commits in this pull request. Is the idea that there should be more or less no user-visible changes? If not, then there should be a changelog...

> What is the point of this file? I added this comment to the commit that adds the file `.dir-locals.el`.