aboutsummaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
Diffstat (limited to 'doc')
-rw-r--r--doc/changelog/04-tactics/11883-fix-autounfold.rst13
-rw-r--r--doc/changelog/04-tactics/12023-master+fixing-empty-Ltac-v-file.rst6
-rw-r--r--doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst5
-rw-r--r--doc/changelog/07-commands-and-options/12034-cumul-sprop.rst5
-rw-r--r--doc/changelog/09-coqide/12060-ide-disable-csd.rst6
-rw-r--r--doc/changelog/10-standard-library/12014-ollibs-vector.rst10
-rw-r--r--doc/changelog/10-standard-library/12031-ollibs-cpermutation.rst4
-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/coqdoc.css338
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst26
-rw-r--r--doc/stdlib/index-list.html.template2
-rw-r--r--doc/tools/docgram/common.edit_mlg18
-rw-r--r--doc/tools/docgram/fullGrammar12
15 files changed, 97 insertions, 1485 deletions
diff --git a/doc/changelog/04-tactics/11883-fix-autounfold.rst b/doc/changelog/04-tactics/11883-fix-autounfold.rst
new file mode 100644
index 0000000000..83ff177380
--- /dev/null
+++ b/doc/changelog/04-tactics/11883-fix-autounfold.rst
@@ -0,0 +1,13 @@
+- **Fixed:**
+ The behavior of :tacn:`autounfold` no longer depends on the names of terms and modules
+ (`#11883 <https://github.com/coq/coq/pull/11883>`_,
+ fixes `#7812 <https://github.com/coq/coq/issues/7812>`_,
+ by Attila Gáspár).
+- **Changed:**
+ `at` clauses can no longer be used with :tacn:`autounfold`. Since they had no effect, it is safe to remove them
+ (`#11883 <https://github.com/coq/coq/pull/11883>`_,
+ by Attila Gáspár).
+- **Changed:**
+ :tacn:`autounfold` no longer fails when the :cmd:`Opaque` command is used on constants in the hint databases
+ (`#11883 <https://github.com/coq/coq/pull/11883>`_,
+ by Attila Gáspár).
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/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst b/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst
new file mode 100644
index 0000000000..7af2b4d97b
--- /dev/null
+++ b/doc/changelog/04-tactics/12116-master+fix12045-missing-reduction-in-using-ind-scheme.rst
@@ -0,0 +1,5 @@
+- **Fixed:**
+ Anomaly with induction schemes whose conclusion is not normalized
+ (`#12116 <https://github.com/coq/coq/pull/12116>`_,
+ by Hugo Herbelin; fixes
+ `#12045 <https://github.com/coq/coq/pull/12045>`_)
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/09-coqide/12060-ide-disable-csd.rst b/doc/changelog/09-coqide/12060-ide-disable-csd.rst
new file mode 100644
index 0000000000..b61ab26007
--- /dev/null
+++ b/doc/changelog/09-coqide/12060-ide-disable-csd.rst
@@ -0,0 +1,6 @@
+- **Changed:**
+ CoqIDE now uses native window frames by default on Windows.
+ The GTK window frames can be restored by setting the `GTK_CSD` environment variable to `1`
+ (`#12060 <https://github.com/coq/coq/pull/12060>`_,
+ fixes `#11080 <https://github.com/coq/coq/issues/11080>`_,
+ by Attila Gáspár).
diff --git a/doc/changelog/10-standard-library/12014-ollibs-vector.rst b/doc/changelog/10-standard-library/12014-ollibs-vector.rst
new file mode 100644
index 0000000000..87625dd23b
--- /dev/null
+++ b/doc/changelog/10-standard-library/12014-ollibs-vector.rst
@@ -0,0 +1,10 @@
+- **Added:**
+ Properties of some operations on vectors:
+
+ - ``nth_order``: ``nth_order_hd``, ``nth_order_tl``, ``nth_order_ext``
+ - ``replace``: ``nth_order_replace_eq``, ``nth_order_replace_neq``, ``replace_id``, ``replace_replace_eq``, ``replace_replace_neq``
+ - ``map``: ``map_id``, ``map_map``, ``map_ext_in``, ``map_ext``
+ - ``Forall`` and ``Forall2``: ``Forall_impl``, ``Forall_forall``, ``Forall_nth_order``, ``Forall2_nth_order``
+
+ (`#12014 <https://github.com/coq/coq/pull/12014>`_,
+ by Olivier Laurent).
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/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/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/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7d031b9b7a..60fdbf0a9d 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -91,9 +91,15 @@ capital letter.
This command supports the :attr:`local`, :attr:`global` and :attr:`export` attributes.
They are described :ref:`here <set_unset_scope_qualifiers>`.
- .. warn:: There is no option @setting_name.
+ .. warn:: There is no flag or option with this name: "@setting_name".
- This message also appears for unknown flags.
+ This warning message can be raised by :cmd:`Set` and
+ :cmd:`Unset` when :n:`@setting_name` is unknown. It is a
+ warning rather than an error because this helps library authors
+ produce Coq code that is compatible with several Coq versions.
+ To preserve the same behavior, they may need to set some
+ compatibility flags or options that did not exist in previous
+ Coq versions.
.. cmd:: Unset @setting_name
:name: Unset
@@ -119,6 +125,20 @@ capital letter.
whether the table contains each specified value, otherise this is equivalent to
:cmd:`Print Table`. The `for` clause is not valid for flags and options.
+ .. exn:: There is no flag, option or table with this name: "@setting_name".
+
+ This error message is raised when calling the :cmd:`Test`
+ command (without the `for` clause), or the :cmd:`Print Table`
+ command, for an unknown :n:`@setting_name`.
+
+ .. exn:: There is no qualid-valued table with this name: "@setting_name".
+ There is no string-valued table with this name: "@setting_name".
+
+ These error messages are raised when calling the :cmd:`Add` or
+ :cmd:`Remove` commands, or the :cmd:`Test` command with the
+ `for` clause, if :n:`@setting_name` is unknown or does not have
+ the right type.
+
.. cmd:: Print Options
Prints the current value of all flags and options, and the names of all tables.
@@ -1076,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/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>:
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
index 5034d9a3c9..700170b3c6 100644
--- a/doc/tools/docgram/common.edit_mlg
+++ b/doc/tools/docgram/common.edit_mlg
@@ -906,14 +906,14 @@ command: [
| DELETE "Unset" option_table
| REPLACE "Set" option_table option_setting
| WITH OPT "Export" "Set" option_table (* set flag *)
-| REPLACE "Test" option_table "for" LIST1 option_ref_value
-| WITH "Test" option_table OPT ( "for" LIST1 option_ref_value )
+| REPLACE "Test" option_table "for" LIST1 table_value
+| WITH "Test" option_table OPT ( "for" LIST1 table_value )
| DELETE "Test" option_table
(* hide the fact that table names are limited to 2 IDENTs *)
-| REPLACE "Add" IDENT IDENT LIST1 option_ref_value
-| WITH "Add" option_table LIST1 option_ref_value
-| DELETE "Add" IDENT LIST1 option_ref_value
+| REPLACE "Add" IDENT IDENT LIST1 table_value
+| WITH "Add" option_table LIST1 table_value
+| DELETE "Add" IDENT LIST1 table_value
| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "symmetry" "proved" "by" constr "as" ident
| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "as" ident
| DELETE "Add" "Parametric" "Relation" binders ":" constr constr "reflexivity" "proved" "by" constr "transitivity" "proved" "by" constr "as" ident
@@ -969,9 +969,9 @@ command: [
| DELETE "Preterm"
(* hide the fact that table names are limited to 2 IDENTs *)
-| REPLACE "Remove" IDENT IDENT LIST1 option_ref_value
-| WITH "Remove" option_table LIST1 option_ref_value
-| DELETE "Remove" IDENT LIST1 option_ref_value
+| REPLACE "Remove" IDENT IDENT LIST1 table_value
+| WITH "Remove" option_table LIST1 table_value
+| DELETE "Remove" IDENT LIST1 table_value
| DELETE "Restore" "State" IDENT
| DELETE "Restore" "State" ne_string
| "Restore" "State" [ IDENT | ne_string ]
@@ -1550,7 +1550,7 @@ SPLICE: [
| constructor_type
| record_binder
| at_level_opt
-| option_ref_value
+| table_value
| positive_search_mark
| in_or_out_modules
| option_setting
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index 04c20a7203..4274dccb40 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -524,12 +524,12 @@ command: [
| "Set" option_table option_setting
| "Unset" option_table
| "Print" "Table" option_table
-| "Add" IDENT IDENT LIST1 option_ref_value
-| "Add" IDENT LIST1 option_ref_value
-| "Test" option_table "for" LIST1 option_ref_value
+| "Add" IDENT IDENT LIST1 table_value
+| "Add" IDENT LIST1 table_value
+| "Test" option_table "for" LIST1 table_value
| "Test" option_table
-| "Remove" IDENT IDENT LIST1 option_ref_value
-| "Remove" IDENT LIST1 option_ref_value
+| "Remove" IDENT IDENT LIST1 table_value
+| "Remove" IDENT LIST1 table_value
| "Write" "State" IDENT
| "Write" "State" ne_string
| "Restore" "State" IDENT
@@ -1318,7 +1318,7 @@ option_setting: [
| STRING
]
-option_ref_value: [
+table_value: [
| global
| STRING
]
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 02:40:43 +0000