"Definition came from this buffer, but precise location is unknown."

[vzaliva]

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."

[cpitclaudel]

Can you give an example file (and your version of Coq?)

[vzaliva]

Coq 8.8.2. I will need to find small enough example for you to reproduce this, but it happening quite often.

[kovach]

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 *)