Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

:CoqGotoDef Broken for Local Definitions with No .vo #363

Open
whonore opened this issue Aug 9, 2024 · 0 comments
Open

:CoqGotoDef Broken for Local Definitions with No .vo #363

whonore opened this issue Aug 9, 2024 · 0 comments
Labels

Comments

@whonore
Copy link
Owner

whonore commented Aug 9, 2024

:CoqGotoDef and the :tag commands fail to find definitions from the current file if there is no corresponding .vo file. This is because definitions are searched using Locate and Locate Library, and the latter only works when there's a .vo file.

@whonore whonore added the bug label Aug 9, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

1 participant