reftex interference

Stream: Emacs

[Yury G. Kudryashov]

I have an Emacs session with some Lean files and some LaTeX files. When I run C-c ) (reftex-reference), then a t (autoref, theorem) in a LaTeX buffer, it tries to modify the *Lean Goal* buffer and fails.

[Yury G. Kudryashov]

If I delete this buffer, then it tries to switch to it anyway, and fails trying to switch to a deleted buffer.