coqdoc - 云端在线

程序：

您的姓名

coqdoc - Coq 证明助手的文档工具

概要

文件 [ 选项 ] 档

商品描述

文件 是 Coq 证明助手的文档工具。 它创建 LaTeX 或 HTML
来自一组 Coq 文件的文档。 有关文档，请参阅 Coq 参考手册 (url
下文）。

配置

整体 选项
-h 帮助。 将为您提供 coqdoc 接受的选项的完整列表。

--html 选择一个 HTML 输出。

- 乳胶
选择一个 LATEX 输出。

--dvi 选择一个 DVI 输出。

--ps 选择 PostScript 输出。

--texmacs
选择一个 TeXmacs 输出。

--标准输出
将输出重定向到标准输出

-o 文件，- 输出 文件
将输出重定向到文件中 文件中。

-d 是， - 目录 DIR
输出文件到目录 DIR 而不是当前目录（选项 -d 不
更改使用选项 -o 指定的文件名（如果有）。

-是的， - 短的
不要为文件插入标题。 默认行为是插入一个标题，如
每个文件的“库 Foo”。

-t 细绳， - 标题 绳子
设置文档标题。

--仅限正文
抑制最终文档的标题和结尾。 因此，您可以插入
生成的文档变成更大的文档。

-p 细绳， - 前言 绳子
在 LATEX 序言中插入一些材料，就在 \begin{document} 之前
（对 -html 毫无意义）。

--vernac 文件 文件， --tex-文件 文件
将文件“file”分别视为 .v（或 .g）文件或 .tex 文件。

--文件来自 文件
读取要在文件“file”中处理的文件名，就好像它们是在命令中给出的一样
线。 对于拆分在多个目录中的程序源很有用。

-q, - 安静的
安静。 除了错误，不要打印任何内容。

-H， - 帮帮我
给出选项的简短摘要并退出。

-v， - 版
打印版本并退出。

索引 选项
默认行为是将仅用于 HTML 输出的索引构建到 index.html 中。

--无索引
不输出索引。

--多索引
为索引中的每个类别和每个字母生成一个页面，以及一个
首页 index.html。

表 of Contents 选项
-toc， - 目录
插入目录。 对于 LATEX 输出，它插入一个 \tableofcontents 在
文档的开头。 对于 HTML 输出，它会构建一个目录
进入 toc.html。

超链接 选项
--glob-来自 文件
从文件文件中使用 Coq 全球化进行引用。 （这种全球化是
使用 Coq 选项 -dump-glob 获得）。

--无外部因素
不要插入到 Coq 标准库的链接。

- 外部的 网址 库根
为根前缀为 libroot 的外部库设置基本 URL。

--coqlib 网址
为 Coq 标准库设置基本 URL（默认为
http://coq.inria.fr/library/).

--coqlib_路径 DIR
设置安装 Coq 文件的基本路径，尤其是样式文件
coqdoc.sty 和 coqdoc.css。

-R DIR 目录
将物理目录 dir 映射到 Coq 逻辑目录 coqdir（类似于 Coq 选项
-R)。 请注意： 选项 -R 仅对命令中它后面的文件有效
行，因此您可能需要首先放置此选项。

内容 选项
-G， --加里纳
不要打印校样。

-l, - 光
光模式。 抑制证明（与 -g 一样）和以下命令：

* [递归] 战术定义
* 提示/提示
* 要求
* 透明/不透明
* 隐式参数/隐式
*部分/变量/假设/结束

选项 -g 和 -l 的行为可以使用 (* begin show
*) ... (* end show *) 环境（见上文）。

语言选择 选项
默认行为是假设 ASCII 7 位输入文件。

-拉丁1， --拉丁语1
选择 ISO-8859-1 输入文件。 相当于 --inputenc latin1 --charset
iso-8859-1。

-utf8, --utf8
选择 UTF-8 (Unicode) 输入文件。 相当于 --inputenc utf8 --charset
utf-8。 可以在以下位置找到 LATEX UTF-8 支持
http://www.ctan.org/tex-archive/macros/latex/contrib/supported/unicode/.

--输入 绳子
给出一个 LATEX 输入编码，作为 LATEX 包 inputenc 的一个选项。

--字符集 绳子
指定要插入 HTML 标题中的 HTML 字符集。

使用 onworks.net 服务在线使用 coqdoc