Skip to content

Commit 5f41092

Browse files
committedJan 24, 2025
Rename PDF refman, and other occurrences of Coq RefMan.
1 parent 7cbac2c commit 5f41092

File tree

11 files changed

+27
-26
lines changed

11 files changed

+27
-26
lines changed
 

‎doc/LICENSE

+7-8
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
1-
The Coq Reference Manual is a collective work from the Coq Development
2-
Team whose members are listed in the file CREDITS of the Coq source
3-
package. All related documents (the LaTeX and BibTeX sources, the
1+
The Rocq Reference Manual is a collective work from the Rocq Development
2+
Team whose members are listed on https://rocq-prover.org/governance.
3+
All related documents (the LaTeX and BibTeX sources, the
44
embedded png files, and the PostScript, PDF and html outputs) are
5-
copyright (c) 1999-2019, Inria, CNRS and contributors, with the
5+
copyright Inria, CNRS and contributors, with the
66
exception of the Ubuntu font file UbuntuMono-B.ttf, which is Copyright
77
2010,2011 Canonical Ltd and licensed under the Ubuntu font license,
88
version 1.0
@@ -17,10 +17,9 @@ the Open Publication License, v1.0 or later (the latest version is
1717
presently available at http://www.opencontent.org/openpub/). Options A
1818
and B are *not* elected.
1919

20-
The Coq Standard Library is a collective work from the Coq Development
21-
Team whose members are listed in the file CREDITS of the Coq source
22-
package. All related documents (the Coq vernacular source files and
23-
the PostScript, PDF and html outputs) are copyright (c) 1999-2019,
20+
The Rocq Core Library is a collective work from the Rocq Development
21+
Team. All related documents (the Rocq vernacular source files and
22+
the PostScript, PDF and html outputs) are copyright
2423
Inria, CNRS and contributors. The material connected to the Standard
2524
Library is distributed under the terms of the Lesser General Public
2625
License version 2.1 or later.

‎doc/common/styles/html/simple/styles.hva

+1-1
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,7 @@
1515
<div id="container">
1616

1717
<div id="header">
18-
<h1>Coq Reference Manual</h1>
18+
<h1>The Rocq Prover Reference Manual</h1>
1919
</div>
2020

2121
<div id="content">

‎doc/dune

+1
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,7 @@
5858
(source_tree sphinx)
5959
(source_tree tools/coqrst)
6060
../config/coq_config.py
61+
../ide/rocqide/coq.png
6162
unreleased.rst
6263
(env_var SPHINXWARNOPT)
6364
(env_var COQRST_EXTRA))

‎doc/sphinx/conf.py

+3-3
Original file line numberDiff line numberDiff line change
@@ -199,7 +199,7 @@ def setup(app):
199199
# Theme options are theme-specific and customize the look and feel of a theme
200200
# further. For a list of options available for each theme, see the
201201
# documentation.
202-
PDF_URL = "https://github.com/coq/coq/releases/download/V{version}/coq-{version}-reference-manual.pdf"
202+
PDF_URL = "https://github.com/coq/coq/releases/download/V{version}/rocq-{version}-reference-manual.pdf"
203203
html_theme_options = {
204204
'collapse_navigation': False
205205
}
@@ -375,11 +375,11 @@ def setup(app):
375375
"_static/coqnotations.sty"
376376
]
377377

378-
latex_documents = [('index', 'CoqRefMan.tex', 'The Coq Reference Manual', author, 'manual')]
378+
latex_documents = [('index', f'rocq-{version}-reference-manual.tex', 'The Rocq Prover Reference Manual', author, 'manual')]
379379

380380
# The name of an image file (relative to this directory) to place at the top of
381381
# the title page.
382-
# latex_logo = "../../ide/coq.png"
382+
latex_logo = "../../ide/rocqide/coq.png"
383383

384384
# If true, show page references after internal links.
385385
#latex_show_pagerefs = False

‎man/coq_makefile.1

+2-2
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,6 @@ Will give you a description of the whole list of options of
3030
.BR coqdep (1)
3131
.PP
3232
.I
33-
The Coq Reference Manual.
33+
The Rocq Prover Reference Manual.
3434
.PP
35-
The Coq web site: http://coq.inria.fr
35+
The Rocq Prover website: https://rocq-prover.org

‎man/coqc.1

+2-2
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,6 @@ Print the compiled file on the standard output.
6161
.BR coqdep (1)
6262
.PP
6363
.I
64-
The Coq Reference Manual.
64+
The Rocq Prover Reference Manual.
6565
.PP
66-
The Coq web site: http://coq.inria.fr
66+
The Rocq Prover website: https://rocq-prover.org

‎man/coqchk.1

+2-2
Original file line numberDiff line numberDiff line change
@@ -104,6 +104,6 @@ Print list of options.
104104
.BR coqdep (1)
105105
.PP
106106
.I
107-
The Coq Reference Manual.
107+
The Rocq Prover Reference Manual.
108108
.PP
109-
The Coq web site: http://coq.inria.fr
109+
The Rocq Prover website: https://rocq-prover.org

‎man/coqdoc.1

+3-2
Original file line numberDiff line numberDiff line change
@@ -221,5 +221,6 @@ Specify the HTML character set, to be inserted in the HTML header.
221221
.SH SEE ALSO
222222
.
223223
.I
224-
The Coq Reference Manual
225-
from http://coq.inria.fr/
224+
The Rocq Prover Reference Manual.
225+
.PP
226+
The Rocq Prover website: https://rocq-prover.org

‎man/coqnative.1

+2-2
Original file line numberDiff line numberDiff line change
@@ -79,6 +79,6 @@ Print list of options.
7979
.BR coqdep (1)
8080
.PP
8181
.I
82-
The Coq Reference Manual.
82+
The Rocq Prover Reference Manual.
8383
.PP
84-
The Coq web site: http://coq.inria.fr
84+
The Rocq Prover website: https://rocq-prover.org

‎man/coqtop.1

+2-2
Original file line numberDiff line numberDiff line change
@@ -165,6 +165,6 @@ Don't load opaque proofs in memory.
165165
.BR coqdep (1)
166166
.PP
167167
.I
168-
The Coq Reference Manual.
168+
The Rocq Prover Reference Manual.
169169
.PP
170-
The Coq web site: http://coq.inria.fr
170+
The Rocq Prover website: https://rocq-prover.org

‎man/coqtop.byte.1

+2-2
Original file line numberDiff line numberDiff line change
@@ -28,6 +28,6 @@ and
2828
.BR coqc (1)
2929
.PP
3030
.I
31-
The Coq Reference Manual.
31+
The Rocq Prover Reference Manual.
3232
.PP
33-
The Coq web site: http://coq.inria.fr
33+
The Rocq Prover website: https://rocq-prover.org

0 commit comments

Comments
 (0)