Skip to content

Commit

Permalink
Documentation of branch “master” at 5f1fc778
Browse files Browse the repository at this point in the history
  • Loading branch information
coqbot committed Jan 21, 2025
1 parent 71541fe commit d83a44f
Show file tree
Hide file tree
Showing 113 changed files with 114 additions and 114 deletions.
Binary file modified master/refman-stdlib/.doctrees/environment.pickle
Binary file not shown.
2 changes: 1 addition & 1 deletion master/refman/.buildinfo
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Sphinx build info version 1
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
config: 31db0873e4bf3152ff241f8c47b4ad2b
config: 899014f35b3bb477b3ad7218f824fab3
tags: 645f666f9bcd5a90fca523b33c5a78b7
Binary file modified master/refman/.doctrees/addendum/extraction.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/addendum/generalized-rewriting.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/addendum/micromega.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/addendum/program.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/addendum/rewrite-rules.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/addendum/ring.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/addendum/universe-polymorphism.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/environment.pickle
Binary file not shown.
Binary file modified master/refman/.doctrees/language/core/assumptions.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/language/core/basic.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/language/core/inductive.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/language/core/modules.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/language/core/records.doctree
Binary file not shown.
Binary file not shown.
Binary file modified master/refman/.doctrees/language/extensions/canonical.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/language/extensions/evars.doctree
Binary file not shown.
Binary file not shown.
Binary file modified master/refman/.doctrees/language/extensions/match.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/proof-engine/ltac.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/proof-engine/ltac2.doctree
Binary file not shown.
Binary file not shown.
Binary file modified master/refman/.doctrees/proof-engine/tactics.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/proof-engine/vernacular-commands.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/proofs/automatic-tactics/auto.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/proofs/automatic-tactics/logic.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/proofs/writing-proofs/equality.doctree
Binary file not shown.
Binary file modified master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree
Binary file not shown.
Binary file not shown.
Binary file not shown.
Binary file modified master/refman/.doctrees/using/libraries/funind.doctree
Binary file not shown.
2 changes: 1 addition & 1 deletion master/refman/addendum/canonical-structures.html
Original file line number Diff line number Diff line change
Expand Up @@ -1293,7 +1293,7 @@

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/extended-pattern-matching.html
Original file line number Diff line number Diff line change
Expand Up @@ -1293,7 +1293,7 @@

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/extraction.html
Original file line number Diff line number Diff line change
Expand Up @@ -2228,7 +2228,7 @@ <h3>Users' Contributions<a class="headerlink" href="#users-contributions" title=

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/generalized-rewriting.html
Original file line number Diff line number Diff line change
Expand Up @@ -2424,7 +2424,7 @@ <h3>Definitions<a class="headerlink" href="#definitions" title="Permalink to thi

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/implicit-coercions.html
Original file line number Diff line number Diff line change
Expand Up @@ -2004,7 +2004,7 @@ <h2>Examples<a class="headerlink" href="#examples" title="Permalink to this head

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/micromega.html
Original file line number Diff line number Diff line change
Expand Up @@ -2090,7 +2090,7 @@ <h2><code class="docutils literal notranslate"><span class="pre">zify</span></co

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/miscellaneous-extensions.html
Original file line number Diff line number Diff line change
Expand Up @@ -1419,7 +1419,7 @@ <h1>Program derivation<a class="headerlink" href="#program-derivation" title="Pe

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/nsatz.html
Original file line number Diff line number Diff line change
Expand Up @@ -1396,7 +1396,7 @@ <h2>More about <code class="docutils literal notranslate"><span class="pre">nsat

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/parallel-proof-processing.html
Original file line number Diff line number Diff line change
Expand Up @@ -1477,7 +1477,7 @@ <h3>Caveats<a class="headerlink" href="#id3" title="Permalink to this heading">

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/program.html
Original file line number Diff line number Diff line change
Expand Up @@ -1771,7 +1771,7 @@

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/rewrite-rules.html
Original file line number Diff line number Diff line change
Expand Up @@ -1475,7 +1475,7 @@ <h2>Level of support<a class="headerlink" href="#level-of-support" title="Permal

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/ring.html
Original file line number Diff line number Diff line change
Expand Up @@ -2127,7 +2127,7 @@ <h2>History of ring<a class="headerlink" href="#history-of-ring" title="Permalin

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/sprop.html
Original file line number Diff line number Diff line change
Expand Up @@ -1658,7 +1658,7 @@ <h2>Debugging <span class="math notranslate nohighlight">\(\SProp\)</span> issue

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/type-classes.html
Original file line number Diff line number Diff line change
Expand Up @@ -2143,7 +2143,7 @@ <h3>Typeclasses eauto<a class="headerlink" href="#typeclasses-eauto" title="Perm

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/addendum/universe-polymorphism.html
Original file line number Diff line number Diff line change
Expand Up @@ -2547,7 +2547,7 @@ <h3>Polymorphic definitions<a class="headerlink" href="#polymorphic-definitions"

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/appendix/history-and-changes/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -1316,7 +1316,7 @@

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/appendix/indexes/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -1321,7 +1321,7 @@

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/changes.html
Original file line number Diff line number Diff line change
Expand Up @@ -15677,7 +15677,7 @@ <h3>Details of changes in 8.0<a class="headerlink" href="#details-of-changes-in-

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/coq-attrindex.html
Original file line number Diff line number Diff line change
Expand Up @@ -1444,7 +1444,7 @@ <h1>Attribute Index</h1>

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/coq-cmdindex.html
Original file line number Diff line number Diff line change
Expand Up @@ -2867,7 +2867,7 @@ <h1>Command Index</h1>

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/coq-exnindex.html
Original file line number Diff line number Diff line change
Expand Up @@ -2903,7 +2903,7 @@ <h1>Errors and Warnings Index</h1>

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/coq-optindex.html
Original file line number Diff line number Diff line change
Expand Up @@ -2033,7 +2033,7 @@ <h1>Flags, options and Tables Index</h1>

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/coq-tacindex.html
Original file line number Diff line number Diff line change
Expand Up @@ -2958,7 +2958,7 @@ <h1>Tactic Index</h1>

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/coq-thmindex.html
Original file line number Diff line number Diff line change
Expand Up @@ -1257,7 +1257,7 @@ <h1>Gallina Index</h1>

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/genindex.html
Original file line number Diff line number Diff line change
Expand Up @@ -4063,7 +4063,7 @@ <h2 id="Z">Z</h2>

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/history.html
Original file line number Diff line number Diff line change
Expand Up @@ -2593,7 +2593,7 @@ <h3>Details of changes in 7.4<a class="headerlink" href="#details-of-changes-in-

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -2864,7 +2864,7 @@ <h2>Contents<a class="headerlink" href="#contents" title="Permalink to this head

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/cic.html
Original file line number Diff line number Diff line change
Expand Up @@ -1802,7 +1802,7 @@ <h1>Typing rules<a class="headerlink" href="#typing-rules" title="Permalink to t

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/coq-library.html
Original file line number Diff line number Diff line change
Expand Up @@ -2090,7 +2090,7 @@ <h3>Tactics<a class="headerlink" href="#tactics" title="Permalink to this headin

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/assumptions.html
Original file line number Diff line number Diff line change
Expand Up @@ -1469,7 +1469,7 @@ <h1>Functions and assumptions<a class="headerlink" href="#functions-and-assumpti

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/basic.html
Original file line number Diff line number Diff line change
Expand Up @@ -1859,7 +1859,7 @@ <h4>Document-level attributes<a class="headerlink" href="#document-level-attribu

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/coinductive.html
Original file line number Diff line number Diff line change
Expand Up @@ -1526,7 +1526,7 @@ <h3>Caveat<a class="headerlink" href="#caveat" title="Permalink to this heading"

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/conversion.html
Original file line number Diff line number Diff line change
Expand Up @@ -1672,7 +1672,7 @@ <h2>Examples<a class="headerlink" href="#examples" title="Permalink to this head

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/definitions.html
Original file line number Diff line number Diff line change
Expand Up @@ -1464,7 +1464,7 @@ <h1>Definitions<a class="headerlink" href="#definitions" title="Permalink to thi

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/index.html
Original file line number Diff line number Diff line change
Expand Up @@ -1344,7 +1344,7 @@

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/inductive.html
Original file line number Diff line number Diff line change
Expand Up @@ -3493,7 +3493,7 @@ <h4>Typing rule<a class="headerlink" href="#id10" title="Permalink to this headi

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/modules.html
Original file line number Diff line number Diff line change
Expand Up @@ -2818,7 +2818,7 @@ <h2>Typing Modules<a class="headerlink" href="#typing-modules" title="Permalink

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/primitive.html
Original file line number Diff line number Diff line change
Expand Up @@ -1485,7 +1485,7 @@ <h1>Primitive objects<a class="headerlink" href="#primitive-objects" title="Perm

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/records.html
Original file line number Diff line number Diff line change
Expand Up @@ -1867,7 +1867,7 @@ <h3>Compatibility Constants for Projections<a class="headerlink" href="#compatib

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/sections.html
Original file line number Diff line number Diff line change
Expand Up @@ -1685,7 +1685,7 @@ <h2>Using sections<a class="headerlink" href="#using-sections" title="Permalink

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/sorts.html
Original file line number Diff line number Diff line change
Expand Up @@ -1366,7 +1366,7 @@

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/core/variants.html
Original file line number Diff line number Diff line change
Expand Up @@ -1602,7 +1602,7 @@ <h3>Private (matching) inductive types<a class="headerlink" href="#private-match

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
2 changes: 1 addition & 1 deletion master/refman/language/extensions/arguments-command.html
Original file line number Diff line number Diff line change
Expand Up @@ -1845,7 +1845,7 @@ <h2>Manual declaration of implicit arguments<a class="headerlink" href="#manual-

<dd><a href="https://rocq-prover.org/doc/v9.0/refman/">9.0</a></dd>

<dd><a href="https://rocq-prover.org/doc/v8.20/refman/">8.20</a></dd>
<dd><a href="https://rocq-prover.org/doc/V8.20.1/refman/">8.20</a></dd>

<dd><a href="https://rocq-prover.org/doc/V8.19.2/refman/">8.19</a></dd>

Expand Down
Loading

0 comments on commit d83a44f

Please sign in to comment.