Install proofgeneral-coq Debian package; this gives you coqtags.

In the root of your soure folder run

 find . -name *.v | xargs coqtags

This gives you a file TAGS

Emacs loads this file and allows you then to jump to definitions using M-.

And back to where you came from using M-*

See http://www.emacswiki.org/emacs/EmacsTags for shortcuts