This is the command coqdep that can be run in the OnWorks free hosting provider using one of our multiple free online workstations such as Ubuntu Online, Fedora Online, Windows online emulator or MAC OS online emulator
coqdep - Compute inter-module dependencies for Coq and Caml programs
coqdep [ -w ] [ -I directory ] [ -coqlib directory ] [ -c ] [ -i ] [ -D ] [ -slash ]
filename ... directory ...
coqdep compute inter-module dependencies for Coq and 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), Declare ML Module commands and Load commands. Dependencies
relative to modules from the Coq library are not printed.
Dependencies of Caml modules are computed by looking at open directives and the dot
-c Prints the dependencies of Caml modules. (On Caml modules, the behaviour is
exactly the same as ocamldep).
-w Prints a warning if a Coq command Declare ML Module is incorrect. (For instance,
you wrote `Declare ML Module "A".', but the module A contains #open "B"). The
correct command is printed (see option -D). The warning is printed on standard
-D This commands looks for every command Declare ML Module of each Coq file given as
argument and complete (if needed) the list of Caml modules. The new command is
printed on the standard output. No dependency is computed with this option.
-slash Prints paths using a slash instead of the OS specific separator. This option is
useful when developping under Cygwin.
The files .v .ml .mli of the directory directory are taken into account during the
calculus of dependencies, but their own dependencies are not printed.
Indicates where is the Coq library. The default value has been determined at
installation time, and therefore this option should not be used under normal
Use coqdep online using onworks.net services