Documentation of branch “master” at 19e3e29b

coq · Dec 11, 2023 · 5849f92 · 5849f92
1 parent b64352c
commit 5849f92
Show file tree

Hide file tree

Showing 130 changed files with 2,251 additions and 2,226 deletions.
diff --git a/master/api/coq-core/Extraction_plugin/Table/index.html b/master/api/coq-core/Extraction_plugin/Table/index.html
diff --git a/master/api/coq-core/Extraction_plugin__Table/index.html b/master/api/coq-core/Extraction_plugin__Table/index.html
diff --git a/master/api/coq-core/System/index.html b/master/api/coq-core/System/index.html
diff --git a/master/refman/.doctrees/addendum/extraction.doctree b/master/refman/.doctrees/addendum/extraction.doctree
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/implicit-coercions.doctree b/master/refman/.doctrees/addendum/implicit-coercions.doctree
diff --git a/master/refman/.doctrees/addendum/micromega.doctree b/master/refman/.doctrees/addendum/micromega.doctree
diff --git a/master/refman/.doctrees/addendum/miscellaneous-extensions.doctree b/master/refman/.doctrees/addendum/miscellaneous-extensions.doctree
diff --git a/master/refman/.doctrees/addendum/program.doctree b/master/refman/.doctrees/addendum/program.doctree
diff --git a/master/refman/.doctrees/addendum/ring.doctree b/master/refman/.doctrees/addendum/ring.doctree
diff --git a/master/refman/.doctrees/addendum/sprop.doctree b/master/refman/.doctrees/addendum/sprop.doctree
diff --git a/master/refman/.doctrees/addendum/type-classes.doctree b/master/refman/.doctrees/addendum/type-classes.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/cic.doctree b/master/refman/.doctrees/language/cic.doctree
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/basic.doctree b/master/refman/.doctrees/language/core/basic.doctree
diff --git a/master/refman/.doctrees/language/core/coinductive.doctree b/master/refman/.doctrees/language/core/coinductive.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/core/records.doctree b/master/refman/.doctrees/language/core/records.doctree
diff --git a/master/refman/.doctrees/language/core/sections.doctree b/master/refman/.doctrees/language/core/sections.doctree
diff --git a/master/refman/.doctrees/language/core/variants.doctree b/master/refman/.doctrees/language/core/variants.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/practical-tools/coq-commands.doctree b/master/refman/.doctrees/practical-tools/coq-commands.doctree
diff --git a/master/refman/.doctrees/practical-tools/coqide.doctree b/master/refman/.doctrees/practical-tools/coqide.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/automatic-tactics/logic.doctree b/master/refman/.doctrees/proofs/automatic-tactics/logic.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/_sources/addendum/extraction.rst.txt b/master/refman/_sources/addendum/extraction.rst.txt
@@ -485,6 +485,11 @@ Additional settings
 
    If this :term:`flag` is set, fully expand Coq types in ML.  See the Coq source code to learn more.
 
+.. opt:: Extraction Output Directory @string
+
+   Sets the directory where extracted files will be written.
+   The default is the current directory, which can be displayed with :cmd:`Pwd`.
+
 Differences between Coq and ML type systems
 ----------------------------------------------
 

diff --git a/master/refman/_sources/practical-tools/coq-commands.rst.txt b/master/refman/_sources/practical-tools/coq-commands.rst.txt
@@ -363,7 +363,7 @@ and ``coqtop``, unless stated otherwise:
        - none
        - none
 
-:-native-output-dir: Set the directory in which to put the aforementioned
+:-native-output-dir *dir*: Set the directory in which to put the aforementioned
   ``.cmxs`` for :tacn:`native_compute`. Defaults to ``.coq-native``.
 :-vos: Indicate Coq to skip the processing of opaque proofs
   (i.e., proofs ending with :cmd:`Qed` or :cmd:`Admitted`), output a ``.vos`` files

diff --git a/master/refman/addendum/canonical-structures.html b/master/refman/addendum/canonical-structures.html
@@ -979,56 +979,56 @@
 </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#id274">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id276">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#id428">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id430">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#id591">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id593">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#id819">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id821">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#id1015">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1017">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#id1179">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1181">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#id1485">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1487">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#id1623">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1625">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>
@@ -1038,22 +1038,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#id1770">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1772">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#id1772">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1774">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#id1773">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1775">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>
@@ -1063,16 +1063,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#id1774">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1776">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#id1775">Summary of changes</a></li>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1776">Potential sources of incompatibilities</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1777">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1778">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>
@@ -1083,32 +1083,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#id1777">Summary of changes</a></li>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1779">Potential sources of incompatibilities</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1779">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1781">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#id1780">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1782">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#id1781">Summary of changes</a></li>
-<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1782">Details of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1783">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1784">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#id1783">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1785">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#id1784">Summary of changes</a></li>
+<li class="toctree-l4"><a class="reference internal" href="../changes.html#id1786">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>