-
Notifications
You must be signed in to change notification settings - Fork 30
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
"Definition came from this buffer, but precise location is unknown." #223
Comments
Can you give an example file (and your version of Coq?) |
Coq 8.8.2. I will need to find small enough example for you to reproduce this, but it happening quite often. |
with Coq 8.14.0, I have an example: Require Import Coq.Init.Nat.
Check Nat.add. (* process up to here. jump to definition takes me to add in Nat.v *)
Require Import Arith.
Check Nat.add. (* now it jumps to PeanoNat.v (because of the include?) *)
Check add. (* this still goes to Nat.v *) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
When I try to jump to a definition in the local buffer by pressing
M-.
I got this error: "Definition came from this buffer, but precise location is unknown."The text was updated successfully, but these errors were encountered: