这是命令 coqdep，可以使用我们的多个免费在线工作站之一在 OnWorks 免费托管服务提供商中运行，例如 Ubuntu Online、Fedora Online、Windows 在线模拟器或 MAC OS 在线模拟器
程序：
您的姓名
coqdep - 计算 Coq 和 Caml 程序的模块间依赖关系
概要
科克德普 [ -w [ -I 目录 [ -coqlib 目录 [ -c [ -i [ -D [ -削减 ]
文件名 ... 目录 ...
商品描述
科克德普 计算 Coq 和 Caml 程序的模块间依赖关系，并打印
以 make 可读的格式依赖于标准输出。 当目录是
作为参数给出，它被递归地查看。
Coq 模块的依赖关系是通过查看来计算的 要求 命令（需要，需要
导出，需要导入）， 声明 ML 模块 命令和 加载 命令。 依赖关系
相对于 Coq 库中的模块没有打印出来。
Caml 模块的依赖关系是通过查看来计算的 打开 指令和点
符号 模块值.
配置
-c 打印 Caml 模块的依赖关系。 （在 Caml 模块上，行为是
与 ocamldep 完全相同）。
-w 如果 Coq 命令打印警告 声明 ML 模块 是不正确的。 （例如，
您编写了`Declare ML Module "A".'，但模块A 包含#open "B")。 这
打印正确的命令（参见选项 -D）。 警告印在标准上
错误。
-D 此命令查找每个命令 声明 ML 模块 每个 Coq 文件给出为
参数并完成（如果需要）Caml 模块的列表。 新命令是
打印在标准输出上。 使用此选项不计算任何依赖项。
-削减 使用斜杠而不是操作系统特定的分隔符打印路径。 这个选项是
在 Cygwin 下开发时很有用。
-I 目录
目录的文件 .v .ml .mli 目录 期间会考虑
依赖关系演算，但不打印它们自己的依赖关系。
-coqlib 目录
指示 Coq 库在哪里。 默认值已确定为
安装时间，因此在正常情况下不应使用此选项
的情况。
使用 onworks.net 服务在线使用 coqdep
