dh_coq is a debhelper program that is responsible for filling the ${coq:Provides} and ${coq:Depends}
substitutions and adding them to substvars files.
It only acts on a single type of binary packages: those shipping Coq theories. Those are usually names
libcoq-XXXX, but neither libcoq-XXX-ocaml nor libcoq-XXX-ocaml-dev: those are OCaml library packages and
managed by dh_ocaml.
On those packages it takes responsibility for, it will look of the Coq compiled files and compute a
checksum. This checksum is stored in the registry in /var/lib/coq/md5sums/, and already allows to say the
current package provides a checksummed-versioned virtual package. The build-depends are then scanned, and
their checksums are retrieved, so the current package depends also on checksummed virtual packages.
The reason for this setup is that without the checksum, with just dependencies on libcoq-XXX, ABI
breakage can happen, because a new libcoq-XXX won't be seen as incompatible, be installed and trigger
incoherent assumptions errors. With fully checksummed packages, apt-get will not upgrade anything until
all packages have migrated to the new ABI.
The dependencies aren't extracted automatically from the compiled project, but from the build-depends of
the built package, so it's crucial that those are accurate.