aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst6
-rw-r--r--doc/changelog/07-commands-and-options/12034-cumul-sprop.rst5
-rw-r--r--doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst4
-rw-r--r--doc/changelog/10-standard-library/12119-issue12119.rst5
-rw-r--r--doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css329
-rw-r--r--doc/common/styles/html/coqremote/sites/all/themes/coq/style.css801
-rw-r--r--doc/sphinx/addendum/sprop.rst7
-rw-r--r--doc/sphinx/changes.rst4
-rw-r--r--doc/sphinx/coqdoc.css338
-rw-r--r--doc/sphinx/proof-engine/tactics.rst103
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst2
-rw-r--r--doc/sphinx/user-extensions/proof-schemes.rst141
-rw-r--r--doc/sphinx/using/libraries/funind.rst237
-rw-r--r--doc/stdlib/index-list.html.template2
14 files changed, 273 insertions, 1711 deletions
diff --git a/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst b/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst
new file mode 100644
index 0000000000..f10208e9b2
--- /dev/null
+++ b/doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+ Tactics with qualified name of the form ``Coq.Init.Notations`` are
+ now qualified with prefix ``Coq.Init.Ltac``; users of the -noinit
+ option should now import Coq.Init.Ltac if they want to use Ltac
+ (`#12023 <https://github.com/coq/coq/pull/12023>`_,
+ by Hugo Herbelin; minor source of incompatibilities).
diff --git a/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst
new file mode 100644
index 0000000000..ad7cf44482
--- /dev/null
+++ b/doc/changelog/07-commands-and-options/12034-cumul-sprop.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+ Added :flag:`Cumulative StrictProp` to control cumulativity of
+ |SProp| and deprecated now redundant command line
+ ``--cumulative-sprop`` (`#12034
+ <https://github.com/coq/coq/pull/12034>`_, by Gaëtan Gilbert).
diff --git a/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst b/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst
new file mode 100644
index 0000000000..95b4cce2f7
--- /dev/null
+++ b/doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst
@@ -0,0 +1,4 @@
+- **Added:**
+ Definition and properties of cyclic permutations / circular shifts: ``CPermutation``
+ (`#12031 <https://github.com/coq/coq/pull/12031>`_,
+ by Olivier Laurent).
diff --git a/doc/changelog/10-standard-library/12119-issue12119.rst b/doc/changelog/10-standard-library/12119-issue12119.rst
new file mode 100644
index 0000000000..42672b1465
--- /dev/null
+++ b/doc/changelog/10-standard-library/12119-issue12119.rst
@@ -0,0 +1,5 @@
+- **Changed:**
+ new lemma ``NoDup_incl_NoDup`` in ``List.v``
+ to remove useless hypothesis `NoDup l'` in ``Sorting.Permutation.NoDup_Permutation_bis``
+ (`#12119 <https://github.com/coq/coq/pull/12119>`_,
+ by Olivier Laurent).
diff --git a/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css b/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css
deleted file mode 100644
index d23ea8f362..0000000000
--- a/doc/common/styles/html/coqremote/sites/all/themes/coq/coqdoc.css
+++ /dev/null
@@ -1,329 +0,0 @@
-body { padding: 0px 0px;
- margin: 0px 0px;
- background-color: white }
-
-#page { display: block;
- padding: 0px;
- margin: 0px;
- padding-bottom: 10px; }
-
-#header { display: block;
- position: relative;
- padding: 0;
- margin: 0;
- vertical-align: middle;
- border-bottom-style: solid;
- border-width: thin }
-
-#header h1 { padding: 0;
- margin: 0;}
-
-
-/* Contents */
-
-#main{ display: block;
- padding: 10px;
- font-family: sans-serif;
- font-size: 100%;
- line-height: 100% }
-
-#main h1 { line-height: 95% } /* allow for multi-line headers */
-
-#main a.idref:visited {color : #416DFF; text-decoration : none; }
-#main a.idref:link {color : #416DFF; text-decoration : none; }
-#main a.idref:hover {text-decoration : none; }
-#main a.idref:active {text-decoration : none; }
-
-#main a.modref:visited {color : #416DFF; text-decoration : none; }
-#main a.modref:link {color : #416DFF; text-decoration : none; }
-#main a.modref:hover {text-decoration : none; }
-#main a.modref:active {text-decoration : none; }
-
-#main .keyword { color : #cf1d1d }
-#main { color: black }
-
-.section { background-color: rgb(60%,60%,100%);
- padding-top: 13px;
- padding-bottom: 13px;
- padding-left: 3px;
- margin-top: 5px;
- margin-bottom: 5px;
- font-size : 175% }
-
-h2.section { background-color: rgb(80%,80%,100%);
- padding-left: 3px;
- padding-top: 12px;
- padding-bottom: 10px;
- font-size : 130% }
-
-h3.section { background-color: rgb(90%,90%,100%);
- padding-left: 3px;
- padding-top: 7px;
- padding-bottom: 7px;
- font-size : 115% }
-
-h4.section {
-/*
- background-color: rgb(80%,80%,80%);
- max-width: 20em;
- padding-left: 5px;
- padding-top: 5px;
- padding-bottom: 5px;
-*/
- background-color: white;
- padding-left: 0px;
- padding-top: 0px;
- padding-bottom: 0px;
- font-size : 100%;
- font-weight : bold;
- text-decoration : underline;
- }
-
-#main .doc { margin: 0px;
- font-family: sans-serif;
- font-size: 100%;
- line-height: 125%;
- max-width: 40em;
- color: black;
- padding: 10px;
- background-color: #90bdff}
-
-.inlinecode {
- display: inline;
-/* font-size: 125%; */
- color: #666666;
- font-family: monospace }
-
-.doc .inlinecode {
- display: inline;
- font-size: 120%;
- color: rgb(30%,30%,70%);
- font-family: monospace }
-
-.doc .inlinecode .id {
- color: rgb(30%,30%,70%);
-}
-
-.inlinecodenm {
- display: inline;
- color: #444444;
-}
-
-.doc .code {
- display: inline;
- font-size: 120%;
- color: rgb(30%,30%,70%);
- font-family: monospace }
-
-.comment {
- display: inline;
- font-family: monospace;
- color: rgb(50%,50%,80%);
-}
-
-.code {
- display: block;
-/* padding-left: 15px; */
- font-size: 110%;
- font-family: monospace;
- }
-
-table.infrule {
- border: 0px;
- margin-left: 50px;
- margin-top: 10px;
- margin-bottom: 10px;
-}
-
-td.infrule {
- font-family: monospace;
- text-align: center;
-/* color: rgb(35%,35%,70%); */
- padding: 0px;
- line-height: 100%;
-}
-
-tr.infrulemiddle hr {
- margin: 1px 0 1px 0;
-}
-
-.infrulenamecol {
- color: rgb(60%,60%,60%);
- font-size: 80%;
- padding-left: 1em;
- padding-bottom: 0.1em
-}
-
-/* Pied de page */
-
-#footer { font-size: 65%;
- font-family: sans-serif; }
-
-/* Identifiers: <span class="id" title="...">) */
-
-.id { display: inline; }
-
-.id[title="constructor"] {
- color: rgb(60%,0%,0%);
-}
-
-.id[title="var"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[title="variable"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[title="definition"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="abbreviation"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="lemma"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="instance"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="projection"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="method"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="inductive"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[title="record"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[title="class"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[title="keyword"] {
- color : #cf1d1d;
-/* color: black; */
-}
-
-/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */
-
-.id[type="constructor"] {
- color: rgb(60%,0%,0%);
-}
-
-.id[type="var"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[type="variable"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[type="definition"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="abbreviation"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="lemma"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="instance"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="projection"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="method"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="inductive"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[type="record"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[type="class"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[type="keyword"] {
- color : #cf1d1d;
-/* color: black; */
-}
-
-.inlinecode .id {
- color: rgb(0%,0%,0%);
-}
-
-
-/* TOC */
-
-#toc h2 {
- padding: 10px;
- background-color: rgb(60%,60%,100%);
-}
-
-#toc li {
- padding-bottom: 8px;
-}
-
-/* Index */
-
-#index {
- margin: 0;
- padding: 0;
- width: 100%;
-}
-
-#index #frontispiece {
- margin: 1em auto;
- padding: 1em;
- width: 60%;
-}
-
-.booktitle { font-size : 140% }
-.authors { font-size : 90%;
- line-height: 115%; }
-.moreauthors { font-size : 60% }
-
-#index #entrance {
- text-align: center;
-}
-
-#index #entrance .spacer {
- margin: 0 30px 0 30px;
-}
-
-#index #footer {
- position: absolute;
- bottom: 0;
-}
-
-.paragraph {
- height: 0.75em;
-}
-
-ul.doclist {
- margin-top: 0em;
- margin-bottom: 0em;
-}
diff --git a/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css b/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css
deleted file mode 100644
index 32c0b33166..0000000000
--- a/doc/common/styles/html/coqremote/sites/all/themes/coq/style.css
+++ /dev/null
@@ -1,801 +0,0 @@
-body
-{
- background: white;
- color:#444;
- font:normal normal normal small/1.5em "Lucida Grande", Verdana, sans-serif;
- margin:0;
- padding:0;
-}
-
-h2
-{
- font-size:150%;
- font-weight:normal;
- margin:20px 0 0;
-}
-
-h3
-{
- font-size:130%;
- font-weight:normal;
-}
-
-a:link,a:visited
-{
- color:#660403;
- font-weight:normal;
- text-decoration:none;
-}
-
-a:hover
-{
- color: red;
- text-decoration:none;
-}
-
-#container
-{
- margin: 0;
- padding: 0;
- }
-
- /*----------header, logo and site name styles----------*/
- #headertop
- {
- display: block;
- /* position:absolute; */
- min-width: 700px;
- top: 0;
- width: 100%;
- height:30px;
- z-index: 1;
- background: transparent url('images/header_top.png') repeat-x;
- }
-
- #header
- {
- min-width: 700px;
- width: 100%; height:70px;
- position: relative;
- left: 0; top: 0;
- background: transparent url('images/header_bot.png') repeat-x;
- }
-
- #logo
- {
- float:left;
- z-index: 2;
- position: absolute;
- top: -15px;
- left: 0px;
- }
-
- #logo img
- {
- border:0;
- float:left;
- }
-
- #logoWrapper
- {
- line-height:4em;
- }
-
- #siteName
- {
- position: relative;
- top: 10px; left: 80px;
- color:#fff;
- float:left;
- font-size:350%;
- }
-
- #siteName a
- {
- color:#fff;
- text-decoration:none;
- }
-
- #siteName a:hover
- {
- color:#ddd;
- text-decoration:none;
- }
-
- #siteSlogan
- {
- color:#eee;
- float:left;
- font-size:170%;
- margin:50px 0 0 10px;
- text-transform:lowercase;
- white-space:nowrap;
- }
-
- /*----------nav styles -- primary links in header----------*/
-
- #nav
-{
- position:absolute; right:0;
- margin: 0;
- padding: 5px;
- }
-
-#nav ul
- {
- list-style:none outside none;
- list-style-image:none;
- margin:0;
- padding:0;
- }
-
- #nav li
- {
- display: inline;
- margin: 0; padding: 4px;
- }
-
- #nav li a
- {
- border:medium none;
- color:#ccc;
- font-weight:normal;
- padding-left:10px;
- padding-right:10px;
- text-decoration:none;
- }
-
- #nav li a:hover
- {
- background:#7B0505 none repeat;
- border:medium none;
- border-left:1px solid #ddd;
- border-right:1px solid #ddd;
- color:#fff;
- padding: 6px 9px 5px 9px;
- }
-
-
-/************** FOOTER *******************/
-
-
-#footer
-{
- background:transparent url('images/footer.png') repeat-x;
- width:100%;
- clear:both;
- font-size:85%;
- text-align:center;
- /* position:fixed; */
- margin: 0;
- padding: 0;
-}
-
-
-#nav-footer
-{
- display: inline;
- color:#444;
- margin: 0;
- padding: 0;
- text-align:right;
- }
-
-#nav-footer ul
- {
- list-style:none outside none;
- list-style-image:none;
- margin:0;
- padding:0px; padding-right: 5px;
- }
-
-#nav-footer li
-{
- display:inline; padding: 4px;
-}
-
- #nav-footer li a
- {
- border:medium none;
- color:#ccc;
- font-size: 11px;
- font-weight:normal;
- padding-left: 10px;
- padding-right: 10px;
- text-decoration:none;
- }
-
- #nav-footer li a:hover
- {
- background:#7B0505 none repeat;
- border:medium none;
- border-left:1px solid #ddd;
- border-right:1px solid #ddd;
- color:#fff;
- margin:0;
- padding: 3px 9px 0px 9px;
- }
-
-
- /*----------main content----------*/
- #content
- {
- display: block;
- position: static;
-
-/* min-width: 640px; */
- max-width: 800px;
-
- margin-left:40px;
- margin-right:300px;
- padding: 2ex 2ex;
-
- z-index:1;
- }
-
-.content {
- display: block;
- position: relative;
-
- margin: 0;
- padding: 0;
-}
-
- /*----------sidebar styles----------*/
- #sidebarWrapper
- {
- /* background:transparent url('images/sidebar_bottom.jpg') no-repeat scroll left bottom;*/
- display:block;
- position:fixed;
- /* avant : top: 100px; right:0px*/
- top: 15px; /* 180 */
- right:0px;
- left: auto;
-
- margin-right: 0px;
-
- /* avant
- width: 12%;
- min-width:80px; */
-
- /* width: 18%; */
- /* min-*/
- width:270px;
-
- z-index:0;
- overflow:hidden;
-
-/* ajout precedent:*/
-/* min-height:320px;
- padding:10px;
- background-image:url('http://www.lix.polytechnique.fr/Labo/Denis.Cousineau/data/coq/rttr340bis.png');
- background-repeat : repeat-x ;*/
-
-/* last ajout */
- /* min-height:510px; */ /* 360 */
- padding-left:0px;
- padding-right:0px;
- padding-top:105px; /* 40 */
- padding-bottom:/*105px*/115px;
- /* background:transparent url('http://www.lix.polytechnique.fr/Labo/Denis.Cousineau/data/coq/trig6b.png') no-repeat scroll left top; */
- background:transparent url('images/sidebarbot.png') no-repeat scroll right bottom;
-
- }
-
-#sidebar {
- padding-left: 40px;
- padding-top: 105px;
- overflow: visible;
- background:transparent url('images/sidebartop.png') no-repeat scroll right top;
-}
-
-#sidebar .title
-{
- /* avant :border-bottom:1px solid #eee;*/
- /* avant : color:#660403;*/
- color:#2D0102;
- font-size:120%;
- font-weight:bold;
- line-height:19px;
- margin:10px 0;
-}
-
-/*----------page styles----------*/
-.pageTitle
-{
- color:#2D0102;
- font-size:220%;
- margin:10px 0 20px;
-}
-
-.mission
-{
- background-color:#efefef;
- border:solid 1px #ccc;
- margin:0 0 10px 0;
- padding:10px;
-}
-
-.messages
-{
- color:#C80000;
- font-size:110%;
- margin:10px 0;
-}
-
-/*----------node styles----------*/
-.nodeTitle
-{
- background: url('images/nodeTitle.gif') no-repeat 0 100%;
- color:#9a0000;
- font-size: 100%;
- margin:0;
-}
-
-.nodeTitle a
-{
- color:#660403;
- text-decoration:none;
-}
-
-.nodeTitle a:hover
-{
- color:#d00000;
- text-decoration:none;
-}
-
-.node
-{
- margin:0 0 20px;
-}
-
-.content p
-{
- margin:10px 0;
-}
-
-.submitted
-{
- color:#a3a3a3;
- font-size:70%;
-}
-
-.nodeLinks
-{
- font-size:95%;
- margin:0;
- padding:0;
-}
-
-.taxonomy
-{
- background:url('icons/tag_red.png') no-repeat 0 7px;
- font-size:80%;
- padding:0 0 5px 16px;
-}
-
-/*----------comment styles----------*/
-.commentTitle
-{
- Border-bottom:1px solid #ddd;
- color:#9a0000;
- font-size:130%;
- margin:20px 0 0;
-}
-
-.commentTitle a
-{
- color:#660403;
- text-decoration:none;
-}
-
-.commentTitle a:hover
-{
- color:#d00000;
- text-decoration:none;
-}
-
-.commentLinks
-{
- background:#f7f7f7;
- border:1px solid #e1e1e1;
- color:#444;
- font-size:95%;
- margin:20px 0 30px;
- padding:4px 0 4px 4px;
-}
-
-
-/*----------img styles----------*/
-img
-{
- padding:3px;
-}
-
-/*----------icons for links----------*/
-.comment_comments a
-{
- background:url('icons/comment.png') no-repeat 0 2px;
- padding-bottom:5px;
- padding-left:20px;
-}
-
-.node_read_more a
-{
- background:url('icons/page_white_go.png') no-repeat;
- padding-bottom:5px;
- padding-left:20px;
-}
-
-.comment_add a,.comment_reply a
-{
- background:url('icons/comment_add.png') no-repeat;
- padding-bottom:5px;
- padding-left:20px;
-}
-.comment_delete a
-{
- background:url('icons/comment_delete.png') no-repeat;
- padding-bottom:5px;
- padding-left:20px;
-}
-
-.comment_edit a
-{
- background:url('icons/comment_edit.png') no-repeat;
- padding-bottom:5px;
- padding-left:20px;
-}
-
-/*----------TinyMCE editor----------*/
-body.mceContentBody
-{
- background:#fff;
- color:#000;
- font-size:12px;
-}
-
-body.mceContentBody a:link
-{
- color:#ff0000;
-}
-
-/*----------table styles----------*/
-table
-{
- margin:1em 0;
- width:100%;
-}
-
-thead th
-{
- border-bottom:2px solid #AAA;
- color:#494949;
- font-weight:bold;
-}
-
-td,th
-{
- padding:.3em 0 .5em;
-}
-
-tr.even,tr.odd,tbody th
-{
- border:solid #D5D6D7;
- border-width:1px 0;
-}
-
-tr.even
-{
- background:#fff;
-}
-
-td.region,td.module,td.container
-{
- background:#D5D6D7;
- border-bottom:1px solid #AAA;
- border-top:1.5em solid #fff;
- color:#455067;
- font-weight:bold;
-}
-
-tr:first-child td.region,tr:first-child td.module,tr:first-child td.container
-{
- border-top-width:0;
-}
-
-td.menu-disabled,td.menu-disabled a
-{
- background-color:#D5C2C2;
- color:#000;
-}
-
-/*----------other styles----------*/
-
-.block
-{
- margin:5px 0 20px;
-}
-
-.thumbnail,.preview
-{
- border:1px solid #ccc;
-}
-
-.lstlisting {
- display: block;
- font-family: monospace;
- white-space: pre;
- margin: 1em 0;
-}
-.center {
- text-align: center;
-}
-.centered {
- display: block-inline;
-}
-
-/*----------download table------------*/
-
-table.downloadtable
-{
- width:90%;
- margin-left:auto;
- margin-right:auto;
-}
-
-table.downloadtable td.downloadheader
-{
-padding: 2px 1em;
-font-weight: bold;
-font-size: 120%;
-color: white;
-background: transparent url('images/header_bot.png') repeat-x;
-/*background-color: #660403; */
-border: solid 2px white;
-border-left: none;
-}
-
-table.downloadtable td.downloadcategory
-{
-padding: 2px 1em;
-background-color: #dfbfbe;
-text-indent: 0;
-}
-
-table.downloadtable td.downloadsize
-{
-text-indent: 0;
-white-space: nowrap;
-height: 52px;
-}
-
-table.downloadtable td
-{
-padding: 2px 1em;
-background-color: #dfbfbe;
-border-right: solid white 2px;
-}
-
-
-table.downloadtable td.downloadtopline
-{
-border-top: solid white 2px;
-}
-
-table.downloadtable td.downloadtoprightline
-{
-border-top: solid 2px white;
-border-right: solid 2px white;
-}
-
-table.downloadtable td.downloadbottomline
-{
-border-bottom: solid 2px white;
-border-right: solid 2px white;
-}
-
-table.downloadtable td.downloadbottomrightline
-{
-border-bottom: solid 2px white;
-border-right: solid 2px white;
-}
-
-table.downloadtable td.downloadrightline
-{
-border-right: solid 2px white;
-}
-
-table.downloadtable td.downloadback
-{
-background-color: #efe4e4;
-}
-
-table.downloadtable td.downloadbottomback
-{
-border-bottom: solid 2px white;
-background-color: #efe4e4;
-}
-
-
-/*********** Normal text style ************/
-
-p {
- text-indent:3em;
-}
-
-ul {
- margin: 0px;
- margin-left:4em;
- padding: 0px;
- list-style-type:square;
-}
-
-li
-{
- text-indent: 0px;
- margin: 0px;
- padding: 0px;
-}
-
-tt { font-size: 1em; }
-
-pre { font-size: 1em; }
-
-/*********** Framework ***********/
-.framework
-{
- display: block;
- position:relative;
- border:solid 1px #660033;
- margin: 8ex 1em; /* 8ex 8ex 1em 1em; */
- padding: 0;
-}
-
-.frameworkcontent
-{
- position:relative;
- left:0px;
-
-
- margin: 0;
- padding: .5ex 2em;
-
- text-indent: 2em;
- text-align: justify;
-}
-
-
-.frameworklabel
-{
- display: inline;
- position:relative;
- top:-1.3ex;
-
- margin-left:2ex;
- padding-top:.4ex;
- padding-bottom:.4ex;
- padding-right:1ex;
- padding-left:1ex;
-
- border: none;
- background: white;
- color: black;
-
- font-weight: bold;
- font-size:115%;
-}
-
-.frameworklinks {
- display:block;
- position:relative;
- top:1.4ex;
-
- margin-right:2ex;
-
- text-align:right;
- font-size:100%
- }
-
-.frameworklinks ul
-{
- display: inline;
- padding: 0px 1ex;
-
- border: none;
- background: white;
-}
-
-
-.frameworklinks li
- {
- display:inline;
- padding: 1ex 0px;
- }
-
- .frameworklinks li a
-{
- border:medium none;
-
- margin: 0px 1ex;
- padding-left:2px;
- padding-right:3px;
-
- font-weight:normal;
- text-decoration:none;
-
- color: #660003;
-}
-
- .frameworklinks li a:hover
- {
- color: red;
-
- border: none;
- }
-
-/* General flat lists */
-.flatlist li {display: inline}
-
-/* For sections in bycat.html */
-.bycatsection dt {
- text-indent: 3em
-}
-
-.bycatsection dt a
-{
- font-weight: bold;
- color:#444;
-}
-
-/* footnote is used in the new contribution form */
-.footnote {
- text-indent: 0pt;
- font-size: 80%;
- color: silver;
- text-align: justify
-}
-
-/****************** CoqIDE Screenshots *****************/
-
-
-.SCpager {
- position:relative;
- top:5px;
- width:630px;
- background: transparent url('images/header_bot.png') repeat-x;
- padding:4px;
-}
-
-.SCpagercontent {
- width:390px;
- position:relative;
- margin-left:auto;
- margin-right:auto;
-}
-
-.SCthumb {
- height:45px;
- margin-left:2px;
- margin-right:2px;
-}
-
-.SCthumbselected {
- height:55px;
- margin-left:2px;
- margin-right:2px;
-}
-
-.SCcontent {
- position:relative;
- top:5px;
- width:638px;
- background-color: #dfbfbe;
-}
-
-.SCscreenshot {
- position:relative;
- height:400px;
- width:auto;
- margin:15px auto 15px 19px;
-}
diff --git a/doc/sphinx/addendum/sprop.rst b/doc/sphinx/addendum/sprop.rst
index 9acdd18b89..b2d3687780 100644
--- a/doc/sphinx/addendum/sprop.rst
+++ b/doc/sphinx/addendum/sprop.rst
@@ -240,3 +240,10 @@ so correctly converts ``x`` and ``y``.
the kernel when it is passed a term with incorrect relevance marks.
To avoid conversion issues as in ``late_mark`` you may wish to use
it to find when your tactics are producing incorrect marks.
+
+.. flag:: Cumulative StrictProp
+ :name: Cumulative StrictProp
+
+ Set this flag (it is off by default) to make the kernel accept
+ cumulativity between |SProp| and other universes. This makes
+ typechecking incomplete.
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst
index 31fb1b7382..ff2b742220 100644
--- a/doc/sphinx/changes.rst
+++ b/doc/sphinx/changes.rst
@@ -481,10 +481,12 @@ Changes in 8.11+beta1
.. _811Reals:
- **Added:**
- Module `Reals.ConstructiveCauchyReals` defines constructive real numbers
+ Module `Reals.Cauchy.ConstructiveCauchyReals` defines constructive real numbers
by Cauchy sequences of rational numbers
(`#10445 <https://github.com/coq/coq/pull/10445>`_, by Vincent Semeria,
with the help and review of Guillaume Melquiond and Bas Spitters).
+ This module is not meant to be imported directly, please import
+ `Reals.Abstract.ConstructiveReals` instead.
- **Added:**
New module `Reals.ClassicalDedekindReals` defines Dedekind real
numbers as boolean-valued functions along with 3 logical axioms:
diff --git a/doc/sphinx/coqdoc.css b/doc/sphinx/coqdoc.css
deleted file mode 100644
index a325a33842..0000000000
--- a/doc/sphinx/coqdoc.css
+++ /dev/null
@@ -1,338 +0,0 @@
-/************************************************************************/
-/* * The Coq Proof Assistant / The Coq Development Team */
-/* v * Copyright INRIA, CNRS and contributors */
-/* <O___,, * (see version control and CREDITS file for authors & dates) */
-/* \VV/ **************************************************************/
-/* // * This file is distributed under the terms of the */
-/* * GNU Lesser General Public License Version 2.1 */
-/* * (see LICENSE file for the text of the license) */
-/************************************************************************/
-body { padding: 0px 0px;
- margin: 0px 0px;
- background-color: white }
-
-#page { display: block;
- padding: 0px;
- margin: 0px;
- padding-bottom: 10px; }
-
-#header { display: block;
- position: relative;
- padding: 0;
- margin: 0;
- vertical-align: middle;
- border-bottom-style: solid;
- border-width: thin }
-
-#header h1 { padding: 0;
- margin: 0;}
-
-
-/* Contents */
-
-#main{ display: block;
- padding: 10px;
- font-family: sans-serif;
- font-size: 100%;
- line-height: 100% }
-
-#main h1 { line-height: 95% } /* allow for multi-line headers */
-
-#main a.idref:visited {color : #416DFF; text-decoration : none; }
-#main a.idref:link {color : #416DFF; text-decoration : none; }
-#main a.idref:hover {text-decoration : none; }
-#main a.idref:active {text-decoration : none; }
-
-#main a.modref:visited {color : #416DFF; text-decoration : none; }
-#main a.modref:link {color : #416DFF; text-decoration : none; }
-#main a.modref:hover {text-decoration : none; }
-#main a.modref:active {text-decoration : none; }
-
-#main .keyword { color : #cf1d1d }
-#main { color: black }
-
-.section { background-color: rgb(60%,60%,100%);
- padding-top: 13px;
- padding-bottom: 13px;
- padding-left: 3px;
- margin-top: 5px;
- margin-bottom: 5px;
- font-size : 175% }
-
-h2.section { background-color: rgb(80%,80%,100%);
- padding-left: 3px;
- padding-top: 12px;
- padding-bottom: 10px;
- font-size : 130% }
-
-h3.section { background-color: rgb(90%,90%,100%);
- padding-left: 3px;
- padding-top: 7px;
- padding-bottom: 7px;
- font-size : 115% }
-
-h4.section {
-/*
- background-color: rgb(80%,80%,80%);
- max-width: 20em;
- padding-left: 5px;
- padding-top: 5px;
- padding-bottom: 5px;
-*/
- background-color: white;
- padding-left: 0px;
- padding-top: 0px;
- padding-bottom: 0px;
- font-size : 100%;
- font-weight : bold;
- text-decoration : underline;
- }
-
-#main .doc { margin: 0px;
- font-family: sans-serif;
- font-size: 100%;
- line-height: 125%;
- max-width: 40em;
- color: black;
- padding: 10px;
- background-color: #90bdff }
-
-.inlinecode {
- display: inline;
-/* font-size: 125%; */
- color: #666666;
- font-family: monospace }
-
-.doc .inlinecode {
- display: inline;
- font-size: 120%;
- color: rgb(30%,30%,70%);
- font-family: monospace }
-
-.doc .inlinecode .id {
- color: rgb(30%,30%,70%);
-}
-
-.inlinecodenm {
- display: inline;
- color: #444444;
-}
-
-.doc .code {
- display: inline;
- font-size: 120%;
- color: rgb(30%,30%,70%);
- font-family: monospace }
-
-.comment {
- display: inline;
- font-family: monospace;
- color: rgb(50%,50%,80%);
-}
-
-.code {
- display: block;
-/* padding-left: 15px; */
- font-size: 110%;
- font-family: monospace;
- }
-
-table.infrule {
- border: 0px;
- margin-left: 50px;
- margin-top: 10px;
- margin-bottom: 10px;
-}
-
-td.infrule {
- font-family: monospace;
- text-align: center;
-/* color: rgb(35%,35%,70%); */
- padding: 0px;
- line-height: 100%;
-}
-
-tr.infrulemiddle hr {
- margin: 1px 0 1px 0;
-}
-
-.infrulenamecol {
- color: rgb(60%,60%,60%);
- font-size: 80%;
- padding-left: 1em;
- padding-bottom: 0.1em
-}
-
-/* Pied de page */
-
-#footer { font-size: 65%;
- font-family: sans-serif; }
-
-/* Identifiers: <span class="id" title="...">) */
-
-.id { display: inline; }
-
-.id[title="constructor"] {
- color: rgb(60%,0%,0%);
-}
-
-.id[title="var"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[title="variable"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[title="definition"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="abbreviation"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="lemma"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="instance"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="projection"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="method"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[title="inductive"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[title="record"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[title="class"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[title="keyword"] {
- color : #cf1d1d;
-/* color: black; */
-}
-
-/* Deprecated rules using the 'type' attribute of <span> (not xhtml valid) */
-
-.id[type="constructor"] {
- color: rgb(60%,0%,0%);
-}
-
-.id[type="var"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[type="variable"] {
- color: rgb(40%,0%,40%);
-}
-
-.id[type="definition"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="abbreviation"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="lemma"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="instance"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="projection"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="method"] {
- color: rgb(0%,40%,0%);
-}
-
-.id[type="inductive"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[type="record"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[type="class"] {
- color: rgb(0%,0%,80%);
-}
-
-.id[type="keyword"] {
- color : #cf1d1d;
-/* color: black; */
-}
-
-.inlinecode .id {
- color: rgb(0%,0%,0%);
-}
-
-
-/* TOC */
-
-#toc h2 {
- padding: 10px;
- background-color: rgb(60%,60%,100%);
-}
-
-#toc li {
- padding-bottom: 8px;
-}
-
-/* Index */
-
-#index {
- margin: 0;
- padding: 0;
- width: 100%;
-}
-
-#index #frontispiece {
- margin: 1em auto;
- padding: 1em;
- width: 60%;
-}
-
-.booktitle { font-size : 140% }
-.authors { font-size : 90%;
- line-height: 115%; }
-.moreauthors { font-size : 60% }
-
-#index #entrance {
- text-align: center;
-}
-
-#index #entrance .spacer {
- margin: 0 30px 0 30px;
-}
-
-#index #footer {
- position: absolute;
- bottom: 0;
-}
-
-.paragraph {
- height: 0.75em;
-}
-
-ul.doclist {
- margin-top: 0em;
- margin-bottom: 0em;
-}
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 7da453b7af..9dcfea4fe7 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -2076,7 +2076,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
Now we are in a contradictory context and the proof can be solved.
- .. coqtop:: all
+ .. coqtop:: all abort
inversion H.
@@ -2104,68 +2104,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`)
See also the larger example of :tacn:`dependent induction`
and an explanation of the underlying technique.
-.. tacn:: function induction (@qualid {+ @term})
- :name: function induction
-
- The tactic functional induction performs case analysis and induction
- following the definition of a function. It makes use of a principle
- generated by ``Function`` (see :ref:`advanced-recursive-functions`) or
- ``Functional Scheme`` (see :ref:`functional-scheme`).
- Note that this tactic is only available after a ``Require Import FunInd``.
-
-.. example::
-
- .. coqtop:: reset all
-
- Require Import FunInd.
- Functional Scheme minus_ind := Induction for minus Sort Prop.
- Check minus_ind.
- Lemma le_minus (n m:nat) : n - m <= n.
- functional induction (minus n m) using minus_ind; simpl; auto.
- Qed.
-
-.. note::
- :n:`(@qualid {+ @term})` must be a correct full application
- of :n:`@qualid`. In particular, the rules for implicit arguments are the
- same as usual. For example use :n:`@qualid` if you want to write implicit
- arguments explicitly.
-
-.. note::
- Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped.
-
-.. note::
- :n:`functional induction (f x1 x2 x3)` is actually a wrapper for
- :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning
- phase, where :n:`@qualid` is the induction principle registered for :g:`f`
- (by the ``Function`` (see :ref:`advanced-recursive-functions`) or
- ``Functional Scheme`` (see :ref:`functional-scheme`)
- command) corresponding to the sort of the goal. Therefore
- ``functional induction`` may fail if the induction scheme :n:`@qualid` is not
- defined. See also :ref:`advanced-recursive-functions` for the function
- terms accepted by ``Function``.
-
-.. note::
- There is a difference between obtaining an induction scheme
- for a function by using :g:`Function` (see :ref:`advanced-recursive-functions`)
- and by using :g:`Functional Scheme` after a normal definition using
- :g:`Fixpoint` or :g:`Definition`. See :ref:`advanced-recursive-functions`
- for details.
-
-.. seealso:: :ref:`advanced-recursive-functions`, :ref:`functional-scheme` and :tacn:`inversion`
-
-.. exn:: Cannot find induction information on @qualid.
- :undocumented:
-
-.. exn:: Not the right number of induction arguments.
- :undocumented:
-
-.. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list
-
- Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving
- explicitly the name of the introduced variables, the induction principle, and
- the values of dependent premises of the elimination scheme, including
- *predicates* for mutual induction when :n:`@qualid` is part of a mutually
- recursive definition.
+.. seealso:: :tacn:`functional induction`
.. tacn:: discriminate @term
:name: discriminate
@@ -2672,6 +2611,8 @@ and an explanation of the underlying technique.
assumption.
Qed.
+.. seealso:: :tacn:`functional inversion`
+
.. tacn:: fix @ident @num
:name: fix
@@ -4604,42 +4545,6 @@ symbol :g:`=`.
Analogous to :tacn:`dependent rewrite ->` but uses the equality from right to
left.
-Inversion
----------
-
-.. tacn:: functional inversion @ident
- :name: functional inversion
-
- :tacn:`functional inversion` is a tactic that performs inversion on hypothesis
- :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid
- {+ @term}` where :n:`@qualid` must have been defined using Function (see
- :ref:`advanced-recursive-functions`). Note that this tactic is only
- available after a ``Require Import FunInd``.
-
- .. exn:: Hypothesis @ident must contain at least one Function.
- :undocumented:
-
- .. exn:: Cannot find inversion information for hypothesis @ident.
-
- This error may be raised when some inversion lemma failed to be generated by
- Function.
-
-
- .. tacv:: functional inversion @num
-
- This does the same thing as :n:`intros until @num` followed by
- :n:`functional inversion @ident` where :token:`ident` is the
- identifier for the last introduced hypothesis.
-
- .. tacv:: functional inversion @ident @qualid
- functional inversion @num @qualid
-
- If the hypothesis :token:`ident` (or :token:`num`) has a type of the form
- :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where
- :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to
- functional inversion, this variant allows choosing which :token:`qualid`
- is inverted.
-
Classical tactics
-----------------
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index a0d1080314..60fdbf0a9d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -1096,6 +1096,8 @@ Controlling Typing Flags
Print the status of the three typing flags: guard checking, positivity checking
and universe checking.
+See also :flag:`Cumulative StrictProp` in the |SProp| chapter.
+
.. example::
.. coqtop:: all reset
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 34197c4fcf..e05be7c2c2 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -190,146 +190,7 @@ Combined Scheme
Check tree_forest_mutrect.
-.. _functional-scheme:
-
-Generation of induction principles with ``Functional`` ``Scheme``
------------------------------------------------------------------
-
-
-.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort}
-
- This command is a high-level experimental tool for
- generating automatically induction principles corresponding to
- (possibly mutually recursive) functions. First, it must be made
- available via ``Require Import FunInd``.
- Each :n:`@ident__i` is a different mutually defined function
- name (the names must be in the same order as when they were defined). This
- command generates the induction principle for each :n:`@ident__i`, following
- the recursive structure and case analyses of the corresponding function
- :n:`@ident__i'`.
-
-.. warning::
-
- There is a difference between induction schemes generated by the command
- :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed,
- :cmd:`Function` generally produces smaller principles that are closer to how
- a user would implement them. See :ref:`advanced-recursive-functions` for details.
-
-.. example::
-
- Induction scheme for div2.
-
- We define the function div2 as follows:
-
- .. coqtop:: all
-
- Require Import FunInd.
- Require Import Arith.
-
- Fixpoint div2 (n:nat) : nat :=
- match n with
- | O => 0
- | S O => 0
- | S (S n') => S (div2 n')
- end.
-
- The definition of a principle of induction corresponding to the
- recursive structure of `div2` is defined by the command:
-
- .. coqtop:: all
-
- Functional Scheme div2_ind := Induction for div2 Sort Prop.
-
- You may now look at the type of div2_ind:
-
- .. coqtop:: all
-
- Check div2_ind.
-
- We can now prove the following lemma using this principle:
-
- .. coqtop:: all
-
- Lemma div2_le' : forall n:nat, div2 n <= n.
- intro n.
- pattern n, (div2 n).
- apply div2_ind; intros.
- auto with arith.
- auto with arith.
- simpl; auto with arith.
- Qed.
-
- We can use directly the functional induction (:tacn:`function induction`) tactic instead
- of the pattern/apply trick:
-
- .. coqtop:: all
-
- Reset div2_le'.
-
- Lemma div2_le : forall n:nat, div2 n <= n.
- intro n.
- functional induction (div2 n).
- auto with arith.
- auto with arith.
- auto with arith.
- Qed.
-
-.. example::
-
- Induction scheme for tree_size.
-
- We define trees by the following mutual inductive type:
-
- .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning
-
- .. coqtop:: reset all
-
- Axiom A : Set.
-
- Inductive tree : Set :=
- node : A -> forest -> tree
- with forest : Set :=
- | empty : forest
- | cons : tree -> forest -> forest.
-
- We define the function tree_size that computes the size of a tree or a
- forest. Note that we use ``Function`` which generally produces better
- principles.
-
- .. coqtop:: all
-
- Require Import FunInd.
-
- Function tree_size (t:tree) : nat :=
- match t with
- | node A f => S (forest_size f)
- end
- with forest_size (f:forest) : nat :=
- match f with
- | empty => 0
- | cons t f' => (tree_size t + forest_size f')
- end.
-
- Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind``
- generated by ``Function`` are not mutual.
-
- .. coqtop:: all
-
- Check tree_size_ind.
-
- Mutual induction principles following the recursive structure of ``tree_size``
- and ``forest_size`` can be generated by the following command:
-
- .. coqtop:: all
-
- Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
- with forest_size_ind2 := Induction for forest_size Sort Prop.
-
- You may now look at the type of `tree_size_ind2`:
-
- .. coqtop:: all
-
- Check tree_size_ind2.
+.. seealso:: :ref:`functional-scheme`
.. _derive-inversion:
diff --git a/doc/sphinx/using/libraries/funind.rst b/doc/sphinx/using/libraries/funind.rst
index ed00f3d455..40f9eedcf0 100644
--- a/doc/sphinx/using/libraries/funind.rst
+++ b/doc/sphinx/using/libraries/funind.rst
@@ -13,7 +13,7 @@ The following command is available when the ``FunInd`` library has been loaded v
This command is a generalization of :cmd:`Fixpoint`. It is a wrapper
for several ways of defining a function *and* other useful related
objects, namely: an induction principle that reflects the recursive
- structure of the function (see :tacn:`function induction`) and its fixpoint equality.
+ structure of the function (see :tacn:`functional induction`) and its fixpoint equality.
This defines a function similar to those defined by :cmd:`Fixpoint`.
As in :cmd:`Fixpoint`, the decreasing argument must
be given (unless the function is not recursive), but it might not
@@ -27,7 +27,7 @@ The following command is available when the ``FunInd`` library has been loaded v
to structurally recursive functions (i.e. when :n:`@fixannot` is a :n:`struct`
clause).
- See :tacn:`function induction` and :cmd:`Functional Scheme` for how to use
+ See :tacn:`functional induction` and :cmd:`Functional Scheme` for how to use
the induction principle to reason easily about the function.
The form of the :n:`@fixannot` clause determines which definition mechanism :cmd:`Function` uses.
@@ -166,4 +166,235 @@ terminating functions.
:tacn:`functional inversion` will not be available for the function.
-.. seealso:: :ref:`functional-scheme` and :tacn:`function induction`
+Tactics
+-------
+
+.. tacn:: functional induction (@qualid {+ @term})
+ :name: functional induction
+
+ The tactic functional induction performs case analysis and induction
+ following the definition of a function. It makes use of a principle
+ generated by :cmd:`Function` or :cmd:`Functional Scheme`.
+ Note that this tactic is only available after a ``Require Import FunInd``.
+
+ .. example::
+
+ .. coqtop:: reset all
+
+ Require Import FunInd.
+ Functional Scheme minus_ind := Induction for minus Sort Prop.
+ Check minus_ind.
+ Lemma le_minus (n m:nat) : n - m <= n.
+ functional induction (minus n m) using minus_ind; simpl; auto.
+ Qed.
+
+ .. note::
+ :n:`(@qualid {+ @term})` must be a correct full application
+ of :n:`@qualid`. In particular, the rules for implicit arguments are the
+ same as usual. For example use :n:`@qualid` if you want to write implicit
+ arguments explicitly.
+
+ .. note::
+ Parentheses around :n:`@qualid {+ @term}` are not mandatory and can be skipped.
+
+ .. note::
+ :n:`functional induction (f x1 x2 x3)` is actually a wrapper for
+ :n:`induction x1, x2, x3, (f x1 x2 x3) using @qualid` followed by a cleaning
+ phase, where :n:`@qualid` is the induction principle registered for :g:`f`
+ (by the :cmd:`Function` or :cmd:`Functional Scheme` command)
+ corresponding to the sort of the goal. Therefore
+ :tacn:`functional induction` may fail if the induction scheme :n:`@qualid` is not
+ defined.
+
+ .. note::
+ There is a difference between obtaining an induction scheme
+ for a function by using :cmd:`Function`
+ and by using :cmd:`Functional Scheme` after a normal definition using
+ :cmd:`Fixpoint` or :cmd:`Definition`.
+
+ .. exn:: Cannot find induction information on @qualid.
+ :undocumented:
+
+ .. exn:: Not the right number of induction arguments.
+ :undocumented:
+
+ .. tacv:: functional induction (@qualid {+ @term}) as @simple_intropattern using @term with @bindings_list
+
+ Similarly to :tacn:`induction` and :tacn:`elim`, this allows giving
+ explicitly the name of the introduced variables, the induction principle, and
+ the values of dependent premises of the elimination scheme, including
+ *predicates* for mutual induction when :n:`@qualid` is part of a mutually
+ recursive definition.
+
+.. tacn:: functional inversion @ident
+ :name: functional inversion
+
+ :tacn:`functional inversion` is a tactic that performs inversion on hypothesis
+ :n:`@ident` of the form :n:`@qualid {+ @term} = @term` or :n:`@term = @qualid
+ {+ @term}` where :n:`@qualid` must have been defined using :cmd:`Function`.
+ Note that this tactic is only available after a ``Require Import FunInd``.
+
+ .. exn:: Hypothesis @ident must contain at least one Function.
+ :undocumented:
+
+ .. exn:: Cannot find inversion information for hypothesis @ident.
+
+ This error may be raised when some inversion lemma failed to be generated by
+ Function.
+
+
+ .. tacv:: functional inversion @num
+
+ This does the same thing as :n:`intros until @num` followed by
+ :n:`functional inversion @ident` where :token:`ident` is the
+ identifier for the last introduced hypothesis.
+
+ .. tacv:: functional inversion @ident @qualid
+ functional inversion @num @qualid
+
+ If the hypothesis :token:`ident` (or :token:`num`) has a type of the form
+ :n:`@qualid__1 {+ @term__i } = @qualid__2 {+ @term__j }` where
+ :n:`@qualid__1` and :n:`@qualid__2` are valid candidates to
+ functional inversion, this variant allows choosing which :token:`qualid`
+ is inverted.
+
+.. _functional-scheme:
+
+Generation of induction principles with ``Functional`` ``Scheme``
+-----------------------------------------------------------------
+
+
+.. cmd:: Functional Scheme @ident__0 := Induction for @ident' Sort @sort {* with @ident__i := Induction for @ident__i' Sort @sort}
+
+ This command is a high-level experimental tool for
+ generating automatically induction principles corresponding to
+ (possibly mutually recursive) functions. First, it must be made
+ available via ``Require Import FunInd``.
+ Each :n:`@ident__i` is a different mutually defined function
+ name (the names must be in the same order as when they were defined). This
+ command generates the induction principle for each :n:`@ident__i`, following
+ the recursive structure and case analyses of the corresponding function
+ :n:`@ident__i'`.
+
+.. warning::
+
+ There is a difference between induction schemes generated by the command
+ :cmd:`Functional Scheme` and these generated by the :cmd:`Function`. Indeed,
+ :cmd:`Function` generally produces smaller principles that are closer to how
+ a user would implement them. See :ref:`advanced-recursive-functions` for details.
+
+.. example::
+
+ Induction scheme for div2.
+
+ We define the function div2 as follows:
+
+ .. coqtop:: all
+
+ Require Import FunInd.
+ Require Import Arith.
+
+ Fixpoint div2 (n:nat) : nat :=
+ match n with
+ | O => 0
+ | S O => 0
+ | S (S n') => S (div2 n')
+ end.
+
+ The definition of a principle of induction corresponding to the
+ recursive structure of `div2` is defined by the command:
+
+ .. coqtop:: all
+
+ Functional Scheme div2_ind := Induction for div2 Sort Prop.
+
+ You may now look at the type of div2_ind:
+
+ .. coqtop:: all
+
+ Check div2_ind.
+
+ We can now prove the following lemma using this principle:
+
+ .. coqtop:: all
+
+ Lemma div2_le' : forall n:nat, div2 n <= n.
+ intro n.
+ pattern n, (div2 n).
+ apply div2_ind; intros.
+ auto with arith.
+ auto with arith.
+ simpl; auto with arith.
+ Qed.
+
+ We can use directly the functional induction (:tacn:`functional induction`) tactic instead
+ of the pattern/apply trick:
+
+ .. coqtop:: all
+
+ Reset div2_le'.
+
+ Lemma div2_le : forall n:nat, div2 n <= n.
+ intro n.
+ functional induction (div2 n).
+ auto with arith.
+ auto with arith.
+ auto with arith.
+ Qed.
+
+.. example::
+
+ Induction scheme for tree_size.
+
+ We define trees by the following mutual inductive type:
+
+ .. original LaTeX had "Variable" instead of "Axiom", which generates an ugly warning
+
+ .. coqtop:: reset all
+
+ Axiom A : Set.
+
+ Inductive tree : Set :=
+ node : A -> forest -> tree
+ with forest : Set :=
+ | empty : forest
+ | cons : tree -> forest -> forest.
+
+ We define the function tree_size that computes the size of a tree or a
+ forest. Note that we use ``Function`` which generally produces better
+ principles.
+
+ .. coqtop:: all
+
+ Require Import FunInd.
+
+ Function tree_size (t:tree) : nat :=
+ match t with
+ | node A f => S (forest_size f)
+ end
+ with forest_size (f:forest) : nat :=
+ match f with
+ | empty => 0
+ | cons t f' => (tree_size t + forest_size f')
+ end.
+
+ Notice that the induction principles ``tree_size_ind`` and ``forest_size_ind``
+ generated by ``Function`` are not mutual.
+
+ .. coqtop:: all
+
+ Check tree_size_ind.
+
+ Mutual induction principles following the recursive structure of ``tree_size``
+ and ``forest_size`` can be generated by the following command:
+
+ .. coqtop:: all
+
+ Functional Scheme tree_size_ind2 := Induction for tree_size Sort Prop
+ with forest_size_ind2 := Induction for forest_size Sort Prop.
+
+ You may now look at the type of `tree_size_ind2`:
+
+ .. coqtop:: all
+
+ Check tree_size_ind2.
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 7fa621c11c..b2c9c936c9 100644
--- a/doc/stdlib/index-list.html.template
+++ b/doc/stdlib/index-list.html.template
@@ -13,6 +13,7 @@ through the <tt>Require Import</tt> command.</p>
The core library (automatically loaded when starting Coq)
</dt>
<dd>
+ theories/Init/Ltac.v
theories/Init/Notations.v
theories/Init/Datatypes.v
theories/Init/Logic.v
@@ -444,6 +445,7 @@ through the <tt>Require Import</tt> command.</p>
theories/Sorting/PermutSetoid.v
theories/Sorting/Mergesort.v
theories/Sorting/Sorted.v
+ theories/Sorting/CPermutation.v
</dd>
<dt> <b>Wellfounded</b>:
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 02:37:21 +0000