12.2 Modules dependencies
In order to compute modules dependencies (so to use make), Coq comes with an appropriate tool, coqdep.coqdep computes inter-module dependencies for Coq and Objective Caml programs, and prints the dependencies on the standard output in a format readable by make. When a directory is given as argument, it is recursively looked at.
Dependencies of Coq modules are computed by looking at Require commands (Require, Require Export, Require Import, Require Implementation), but also at the command Declare ML Module.
Dependencies of Objective Caml modules are computed by looking at
open commands and the dot notation module.value.See the man page of coqdep for more details and options.