Documentation of branch “master” at 7075d637

coq · Jan 22, 2024 · 1397486 · 1397486
1 parent 536e30c
commit 1397486
Show file tree

Hide file tree

Showing 109 changed files with 2,347 additions and 2,345 deletions.
diff --git a/master/refman/.doctrees/addendum/generalized-rewriting.doctree b/master/refman/.doctrees/addendum/generalized-rewriting.doctree
diff --git a/master/refman/.doctrees/addendum/program.doctree b/master/refman/.doctrees/addendum/program.doctree
diff --git a/master/refman/.doctrees/addendum/universe-polymorphism.doctree b/master/refman/.doctrees/addendum/universe-polymorphism.doctree
diff --git a/master/refman/.doctrees/changes.doctree b/master/refman/.doctrees/changes.doctree
diff --git a/master/refman/.doctrees/environment.pickle b/master/refman/.doctrees/environment.pickle
diff --git a/master/refman/.doctrees/language/coq-library.doctree b/master/refman/.doctrees/language/coq-library.doctree
diff --git a/master/refman/.doctrees/language/core/assumptions.doctree b/master/refman/.doctrees/language/core/assumptions.doctree
diff --git a/master/refman/.doctrees/language/core/conversion.doctree b/master/refman/.doctrees/language/core/conversion.doctree
diff --git a/master/refman/.doctrees/language/core/inductive.doctree b/master/refman/.doctrees/language/core/inductive.doctree
diff --git a/master/refman/.doctrees/language/core/modules.doctree b/master/refman/.doctrees/language/core/modules.doctree
diff --git a/master/refman/.doctrees/language/core/primitive.doctree b/master/refman/.doctrees/language/core/primitive.doctree
diff --git a/master/refman/.doctrees/language/extensions/arguments-command.doctree b/master/refman/.doctrees/language/extensions/arguments-command.doctree
diff --git a/master/refman/.doctrees/language/extensions/canonical.doctree b/master/refman/.doctrees/language/extensions/canonical.doctree
diff --git a/master/refman/.doctrees/language/extensions/evars.doctree b/master/refman/.doctrees/language/extensions/evars.doctree
diff --git a/master/refman/.doctrees/language/extensions/implicit-arguments.doctree b/master/refman/.doctrees/language/extensions/implicit-arguments.doctree
diff --git a/master/refman/.doctrees/language/extensions/match.doctree b/master/refman/.doctrees/language/extensions/match.doctree
diff --git a/master/refman/.doctrees/proof-engine/ltac.doctree b/master/refman/.doctrees/proof-engine/ltac.doctree
diff --git a/master/refman/.doctrees/proof-engine/ltac2.doctree b/master/refman/.doctrees/proof-engine/ltac2.doctree
diff --git a/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree b/master/refman/.doctrees/proof-engine/ssreflect-proof-language.doctree
diff --git a/master/refman/.doctrees/proof-engine/tactics.doctree b/master/refman/.doctrees/proof-engine/tactics.doctree
diff --git a/master/refman/.doctrees/proof-engine/vernacular-commands.doctree b/master/refman/.doctrees/proof-engine/vernacular-commands.doctree
diff --git a/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree b/master/refman/.doctrees/proofs/automatic-tactics/auto.doctree
diff --git a/master/refman/.doctrees/proofs/writing-proofs/equality.doctree b/master/refman/.doctrees/proofs/writing-proofs/equality.doctree
diff --git a/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree b/master/refman/.doctrees/proofs/writing-proofs/proof-mode.doctree
diff --git a/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree b/master/refman/.doctrees/proofs/writing-proofs/reasoning-inductives.doctree
diff --git a/master/refman/.doctrees/user-extensions/syntax-extensions.doctree b/master/refman/.doctrees/user-extensions/syntax-extensions.doctree
diff --git a/master/refman/.doctrees/using/libraries/funind.doctree b/master/refman/.doctrees/using/libraries/funind.doctree
diff --git a/master/refman/.doctrees/using/libraries/writing.doctree b/master/refman/.doctrees/using/libraries/writing.doctree
diff --git a/master/refman/addendum/canonical-structures.html b/master/refman/addendum/canonical-structures.html
@@ -979,61 +979,61 @@
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-18">Version 8.18</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id166">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id167">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-18-0">Changes in 8.18.0</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-17">Version 8.17</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id308">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id309">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-17-0">Changes in 8.17.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-17-1">Changes in 8.17.1</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-16">Version 8.16</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id468">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id469">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-16-0">Changes in 8.16.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-16-1">Changes in 8.16.1</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-15">Version 8.15</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id631">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id632">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-15-0">Changes in 8.15.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-15-1">Changes in 8.15.1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-15-2">Changes in 8.15.2</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-14">Version 8.14</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id859">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id860">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-14-0">Changes in 8.14.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-14-1">Changes in 8.14.1</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-13">Version 8.13</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1055">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1056">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-13-beta1">Changes in 8.13+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-13-0">Changes in 8.13.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-13-1">Changes in 8.13.1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-13-2">Changes in 8.13.2</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-12">Version 8.12</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1219">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1220">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-12-beta1">Changes in 8.12+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-12-0">Changes in 8.12.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-12-1">Changes in 8.12.1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-12-2">Changes in 8.12.2</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-11">Version 8.11</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1525">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1526">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-11-beta1">Changes in 8.11+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-11-0">Changes in 8.11.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-11-1">Changes in 8.11.1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-11-2">Changes in 8.11.2</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-10">Version 8.10</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1663">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1664">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#other-changes-in-8-10-beta1">Other changes in 8.10+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-10-beta2">Changes in 8.10+beta2</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-10-beta3">Changes in 8.10+beta3</a></li>
@@ -1043,22 +1043,22 @@
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-9">Version 8.9</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1810">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1811">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-9-beta1">Details of changes in 8.9+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-8-0">Changes in 8.8.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#changes-in-8-8-1">Changes in 8.8.1</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-8">Version 8.8</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1812">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1813">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-8-beta1">Details of changes in 8.8+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-8-0">Details of changes in 8.8.0</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-8-1">Details of changes in 8.8.1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-8-2">Details of changes in 8.8.2</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-7">Version 8.7</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1813">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1814">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#potential-compatibility-issues">Potential compatibility issues</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-7-beta1">Details of changes in 8.7+beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-7-beta2">Details of changes in 8.7+beta2</a></li>
@@ -1068,16 +1068,16 @@
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-6">Version 8.6</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1814">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1815">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#potential-sources-of-incompatibilities">Potential sources of incompatibilities</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-6beta1">Details of changes in 8.6beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-6">Details of changes in 8.6</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-6-1">Details of changes in 8.6.1</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-5">Version 8.5</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1815">Summary of changes</a></li>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1816">Potential sources of incompatibilities</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1816">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1817">Potential sources of incompatibilities</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-5beta1">Details of changes in 8.5beta1</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-5beta2">Details of changes in 8.5beta2</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-5beta3">Details of changes in 8.5beta3</a></li>
@@ -1088,32 +1088,32 @@
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-4">Version 8.4</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1817">Summary of changes</a></li>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1819">Potential sources of incompatibilities</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1818">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1820">Potential sources of incompatibilities</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-4beta">Details of changes in 8.4beta</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-4beta2">Details of changes in 8.4beta2</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-4">Details of changes in 8.4</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-3">Version 8.3</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1820">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1821">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes">Details of changes</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-2">Version 8.2</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1821">Summary of changes</a></li>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1822">Details of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1822">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1823">Details of changes</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-1">Version 8.1</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1823">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1824">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-1beta">Details of changes in 8.1beta</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-1gamma">Details of changes in 8.1gamma</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-1">Details of changes in 8.1</a></li>
 </ul>
 </li>
 <li class="toctree-l3"><a class="reference internal" href="../changes.html#version-8-0">Version 8.0</a><ul>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1824">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1825">Summary of changes</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-0beta-old-syntax">Details of changes in 8.0beta old syntax</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-0beta-new-syntax">Details of changes in 8.0beta new syntax</a></li>
 <li class="toctree-l4"><a class="reference internal" href="../changes.html#details-of-changes-in-8-0">Details of changes in 8.0</a></li>