diff options
Diffstat (limited to 'doc')
47 files changed, 587 insertions, 1816 deletions
diff --git a/doc/changelog/01-kernel/11972-fix-require-in-section.rst b/doc/changelog/01-kernel/11972-fix-require-in-section.rst new file mode 100644 index 0000000000..7a2fa9185f --- /dev/null +++ b/doc/changelog/01-kernel/11972-fix-require-in-section.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Using :cmd:`Require` inside a section caused an anomaly when closing + the section. (`#11972 <https://github.com/coq/coq/pull/11972>`_, by + Gaëtan Gilbert, fixing `#11783 + <https://github.com/coq/coq/issues/11783>`_, reported by Attila + Boros). diff --git a/doc/changelog/04-tactics/11023-nativecompute-timing.rst b/doc/changelog/04-tactics/11023-nativecompute-timing.rst deleted file mode 100644 index e8cdfcca21..0000000000 --- a/doc/changelog/04-tactics/11023-nativecompute-timing.rst +++ /dev/null @@ -1,7 +0,0 @@ -- The :flag:`NativeCompute Timing` flag causes calls to - :tacn:`native_compute` (as well as kernel calls to the native - compiler) to emit separate timing information about compilation, - execution, and reification. It replaces the timing information - previously emitted when the `-debug` flag was set, and allows more - fine-grained timing of the native compiler (`#11023 - <https://github.com/coq/coq/pull/11023>`_, by Jason Gross). diff --git a/doc/changelog/04-tactics/11025-nativecompute-timing.rst b/doc/changelog/04-tactics/11025-nativecompute-timing.rst new file mode 100644 index 0000000000..cb77457c31 --- /dev/null +++ b/doc/changelog/04-tactics/11025-nativecompute-timing.rst @@ -0,0 +1,11 @@ +- **Changed:** The :flag:`NativeCompute Timing` flag causes calls to + :tacn:`native_compute` (as well as kernel calls to the native + compiler) to emit separate timing information about conversion to + native code, compilation, execution, and reification. It replaces + the timing information previously emitted when the `-debug` flag was + set, and allows more fine-grained timing of the native compiler + (`#11025 <https://github.com/coq/coq/pull/11025>`_, by Jason Gross). + Additionally, the timing information now uses real time rather than + user time (Fixes `#11962 + <https://github.com/coq/coq/issues/11962>`_, `#11963 + <https://github.com/coq/coq/pull/11963>`_, by Jason Gross) 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/11976-deprecate-omega.rst b/doc/changelog/04-tactics/11976-deprecate-omega.rst new file mode 100644 index 0000000000..59c9612d17 --- /dev/null +++ b/doc/changelog/04-tactics/11976-deprecate-omega.rst @@ -0,0 +1,5 @@ +- **Deprecated:** + The :tacn:`omega` tactic is deprecated; + use :tacn:`lia` from the :ref:`Micromega <micromega>` plugin instead + (`#11976 <https://github.com/coq/coq/pull/11976>`_, + by Vincent Laporte). 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/07-commands-and-options/12070-native-compiler-disabled.rst b/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst new file mode 100644 index 0000000000..0f30b5f5e8 --- /dev/null +++ b/doc/changelog/07-commands-and-options/12070-native-compiler-disabled.rst @@ -0,0 +1,5 @@ +- **Changed:** + Ignore -native-compiler option when built without native compute + support. + (`#12070 <https://github.com/coq/coq/pull/12070>`_, + by Pierre Roux). diff --git a/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst b/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst new file mode 100644 index 0000000000..5c4ef82b8b --- /dev/null +++ b/doc/changelog/08-tools/12026-master+coqdoc-self-linked-defs-wish7093.rst @@ -0,0 +1,4 @@ +- **Added:** + Definitions in coqdoc link to themselves, giving access in html to their own url + (`#12026 <https://github.com/coq/coq/pull/12026>`_, + by Hugo Herbelin; granting `#7093 <https://github.com/coq/coq/pull/7093>`_). diff --git a/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst b/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst new file mode 100644 index 0000000000..af0d28305a --- /dev/null +++ b/doc/changelog/08-tools/12033-master+coqdoc-fix7697-passing-binders-location.rst @@ -0,0 +1,5 @@ +- **Added:** + Add hyperlinks on bound variables for coqdoc + (`#12033 <https://github.com/coq/coq/pull/12033>`_, + by Hugo Herbelin; it incidentally fixes + `#7697 <https://github.com/coq/coq/pull/7697>`_). diff --git a/doc/changelog/08-tools/12037-coqdoc-preformatted.rst b/doc/changelog/08-tools/12037-coqdoc-preformatted.rst new file mode 100644 index 0000000000..bf65719516 --- /dev/null +++ b/doc/changelog/08-tools/12037-coqdoc-preformatted.rst @@ -0,0 +1,6 @@ +- **Fixed:** + ``coqdoc`` now reports the location of a mismatched opening ``[[`` instead of + throwing an uninformative exception. + (`#12037 <https://github.com/coq/coq/pull/12037>`_, + fixes `#9670 <https://github.com/coq/coq/issues/9670>`_, + by Lysxia). diff --git a/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst b/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst new file mode 100644 index 0000000000..f6af5d40e8 --- /dev/null +++ b/doc/changelog/08-tools/12091-master+coqdoc-css-target.rst @@ -0,0 +1,4 @@ +- **Added:** + ``Coqdoc``: Highlighting of the exact position of the target of links + (`#12091 <https://github.com/coq/coq/pull/12091>`_, + by Hugo Herbelin). diff --git a/doc/changelog/08-tools/12126-adjust-timed-name.rst b/doc/changelog/08-tools/12126-adjust-timed-name.rst new file mode 100644 index 0000000000..c305b384d9 --- /dev/null +++ b/doc/changelog/08-tools/12126-adjust-timed-name.rst @@ -0,0 +1,8 @@ +- **Changed:** + The output of ``make TIMED=1`` (and therefore the timing targets + such as ``print-pretty-timed`` and ``print-pretty-timed-diff``) now + displays the full name of the output file being built, rather than + the stem of the rule (which was usually the filename without the + extension, but in general could be anything for user-defined rules + involving ``%``) (`#12126 + <https://github.com/coq/coq/pull/12126>`_, by Jason Gross). 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/09-coqide/12106-master+coqide-style-apply-all-windows.rst b/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst new file mode 100644 index 0000000000..6b1148a9a8 --- /dev/null +++ b/doc/changelog/09-coqide/12106-master+coqide-style-apply-all-windows.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Highlighting style consistently applied to all three buffers of CoqIDE + (`#12106 <https://github.com/coq/coq/pull/12106>`_, + by Hugo Herbelin; fixes + `#11506 <https://github.com/coq/coq/pull/11506>`_). diff --git a/doc/changelog/10-standard-library/11957-signotations.rst b/doc/changelog/10-standard-library/11957-signotations.rst new file mode 100644 index 0000000000..fc5d434274 --- /dev/null +++ b/doc/changelog/10-standard-library/11957-signotations.rst @@ -0,0 +1,4 @@ +- **Added:** + notations for sigma types: ``{ x & P & Q }``, ``{ ' pat & P }``, ``{ ' pat & P & Q }`` + (`#11957 <https://github.com/coq/coq/pull/11957>`_, + by Olivier Laurent). 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/changelog/10-standard-library/12044-issue-12015.rst b/doc/changelog/10-standard-library/12044-issue-12015.rst new file mode 100644 index 0000000000..166fc80fb0 --- /dev/null +++ b/doc/changelog/10-standard-library/12044-issue-12015.rst @@ -0,0 +1,10 @@ +- **Fixed:** + Rewrote ``Structures.OrderedTypeEx.String_as_OT.compare`` + to avoid huge proof terms + (Fixes `#12015 <https://github.com/coq/coq/issues/12015>`_, + `#12044 <https://github.com/coq/coq/pull/12044>`_, + by formalize.eth (formalize@protonmail.com)). +- **Added:** + Added ``Structures.OrderedTypeEx.Ascii_as_OT`` + (`#12044 <https://github.com/coq/coq/pull/12044>`_, + by formalize.eth (formalize@protonmail.com)). 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/plugin_tutorial/tuto1/src/g_tuto1.mlg b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg index 73d94c2a51..8c2090f3be 100644 --- a/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg +++ b/doc/plugin_tutorial/tuto1/src/g_tuto1.mlg @@ -286,8 +286,8 @@ END VERNAC COMMAND EXTEND ExploreProof CLASSIFIED AS QUERY | ![ proof_query ] [ "ExploreProof" ] -> { fun ~pstate -> - let sigma, env = Pfedit.get_current_context pstate in - let pprf = Proof.partial_proof (Proof_global.get_proof pstate) in + let sigma, env = Declare.get_current_context pstate in + let pprf = Proof.partial_proof (Declare.Proof.get_proof pstate) in Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl (Printer.pr_econstr_env env sigma) pprf) } diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml index 8c4dc0e8a6..b94b1fc657 100644 --- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml +++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml @@ -1,8 +1,6 @@ -let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt = - DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook - ~opaque ~poly ~udecl ~types:tyopt ~body sigma - let declare_definition ~poly name sigma body = let udecl = UState.default_univ_decl in - edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) - ~kind:Decls.(IsDefinition Definition) ~opaque:false ~impargs:[] ~udecl sigma body None + let scope = DeclareDef.Global Declare.ImportDefaultBehavior in + let kind = Decls.(IsDefinition Definition) in + DeclareDef.declare_definition ~name ~scope ~kind ~impargs:[] ~udecl + ~opaque:false ~poly ~types:None ~body sigma diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst index f706633da9..77bf58aac6 100644 --- a/doc/sphinx/addendum/micromega.rst +++ b/doc/sphinx/addendum/micromega.rst @@ -1,4 +1,4 @@ -.. _ micromega: +.. _micromega: Micromega: tactics for solving arithmetic goals over ordered rings ================================================================== diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index daca43e65e..e1b1ee8e8d 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -1,4 +1,4 @@ -.. _omega: +.. _omega_chapter: Omega: a solver for quantifier-free problems in Presburger Arithmetic ===================================================================== @@ -7,20 +7,18 @@ Omega: a solver for quantifier-free problems in Presburger Arithmetic .. warning:: - The :tacn:`omega` tactic is about to be deprecated in favor of the - :tacn:`lia` tactic. The goal is to consolidate the arithmetic - solving capabilities of Coq into a single engine; moreover, - :tacn:`lia` is in general more powerful than :tacn:`omega` (it is a - complete Presburger arithmetic solver while :tacn:`omega` was known - to be incomplete). - - Work is in progress to make sure that there are no regressions - (including no performance regression) when switching from - :tacn:`omega` to :tacn:`lia` in existing projects. However, we - already recommend using :tacn:`lia` in new or refactored proof - scripts. We also ask that you report (in our `bug tracker - <https://github.com/coq/coq/issues>`_) any issue you encounter, - especially if the issue was not present in :tacn:`omega`. + The :tacn:`omega` tactic is deprecated in favor of the :tacn:`lia` + tactic. The goal is to consolidate the arithmetic solving + capabilities of Coq into a single engine; moreover, :tacn:`lia` is + in general more powerful than :tacn:`omega` (it is a complete + Presburger arithmetic solver while :tacn:`omega` was known to be + incomplete). + + It is recommended to switch from :tacn:`omega` to :tacn:`lia` in existing + projects. We also ask that you report (in our `bug tracker + <https://github.com/coq/coq/issues>`_) any issue you encounter, especially + if the issue was not present in :tacn:`omega`. If no new issues are + reported, :tacn:`omega` will be removed soon. Note that replacing :tacn:`omega` with :tacn:`lia` can break non-robust proof scripts which rely on incompleteness bugs of @@ -30,6 +28,11 @@ Description of ``omega`` ------------------------ .. tacn:: omega + :name: omega + + .. deprecated:: 8.12 + + Use :tacn:`lia` instead. :tacn:`omega` is a tactic for solving goals in Presburger arithmetic, i.e. for proving formulas made of equations and inequalities over the @@ -118,7 +121,7 @@ loaded by .. example:: - .. coqtop:: all + .. coqtop:: all warn Require Import Omega. 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/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index a08495badd..2958d866ac 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -227,7 +227,7 @@ constraints by prefixing the level names with symbols. Because inductive subtypings are only produced by comparing inductives to themselves with universes changed, they amount to variance information: each universe is either invariant, covariant or -irrelevant (there are no contravariant subtypings in Coq), +irrelevant (there are no contravariant subtypings in |Coq|), respectively represented by the symbols `=`, `+` and `*`. Here we see that :g:`list` binds an irrelevant universe, so any two @@ -426,6 +426,19 @@ mode, introduced universe names can be referred to in terms. Note that local universe names shadow global universe names. During a proof, one can use :cmd:`Show Universes` to display the current context of universes. +It is possible to provide only some universe levels and let |Coq| infer the others +by adding a :g:`+` in the list of bound universe levels: + +.. coqtop:: all + + Fail Definition foobar@{u} : Type@{u} := Type. + Definition foobar@{u +} : Type@{u} := Type. + Set Printing Universes. + Print foobar. + +This can be used to find which universes need to be explicitly bound in a given +definition. + Definitions can also be instantiated explicitly, giving their full instance: diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 31fb1b7382..6615b98660 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -55,7 +55,8 @@ __ 811Reals_ Additionally, while the :tacn:`omega` tactic is not yet deprecated in this version of Coq, it should soon be the case and we already recommend users to switch to :tacn:`lia` in new proof scripts (see -also the warning message in the :ref:`corresponding chapter <omega>`). +also the warning message in the :ref:`corresponding chapter +<omega_chapter>`). The ``dev/doc/critical-bugs`` file documents the known critical bugs of |Coq| and affected releases. See the `Changes in 8.11+beta1`_ @@ -481,10 +482,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/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 78b1f02383..57c8683aaa 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -422,7 +422,12 @@ are now available through the dot notation. If :n:`@module_binder`\s are specified, declares a functor with parameters given by the list of :token:`module_binder`\s. -.. cmd:: Import {+ @qualid } +.. cmd:: Import {+ @filtered_import } + + .. insertprodn filtered_import filtered_import + + .. prodn:: + filtered_import ::= @qualid {? ( {+, @qualid {? ( .. ) } } ) } If :token:`qualid` denotes a valid basic module (i.e. its module type is a signature), makes its components available by their short names. @@ -465,12 +470,50 @@ are now available through the dot notation. Check B.T. -.. cmd:: Export {+ @qualid } + Appending a module name with a parenthesized list of names will + make only those names available with short names, not other names + defined in the module nor will it activate other features. + + The names to import may be constants, inductive types and + constructors, and notation aliases (for instance, Ltac definitions + cannot be selectively imported). If they are from an inner module + to the one being imported, they must be prefixed by the inner path. + + The name of an inductive type may also be followed by ``(..)`` to + import it, its constructors and its eliminators if they exist. For + this purpose "eliminator" means a constant in the same module whose + name is the inductive type's name suffixed by one of ``_sind``, + ``_ind``, ``_rec`` or ``_rect``. + + .. example:: + + .. coqtop:: reset in + + Module A. + Module B. + Inductive T := C. + Definition U := nat. + End B. + Definition Z := Prop. + End A. + Import A(B.T(..), Z). + + .. coqtop:: all + + Check B.T. + Check B.C. + Check Z. + Fail Check B.U. + Check A.B.U. + +.. cmd:: Export {+ @filtered_import } :name: Export Similar to :cmd:`Import`, except that when the module containing this command is imported, the :n:`{+ @qualid }` are imported as well. + The selective import syntax also works with Export. + .. exn:: @qualid is not a module. :undocumented: diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index ab3d70eaca..a045120b70 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -1,3 +1,5 @@ +.. |GtkSourceView| replace:: :smallcaps:`GtkSourceView` + .. _coqintegrateddevelopmentenvironment: |Coq| Integrated Development Environment @@ -145,7 +147,18 @@ presented as a notebook. The first section is for selecting the text font used for scripts, goal and message windows. -The second and third sections are for controlling colors and style. +The second and third sections are for controlling colors and style of +the three main buffers. A predefined |Coq| highlighting style as well +as standard |GtkSourceView| styles are available. Other styles can be +added e.g. in ``$HOME/.local/share/gtksourceview-3.0/styles/`` (see +the general documentation about |GtkSourceView| for the various +possibilities). Note that the style of the rest of graphical part of +Coqide is not under the control of |GtkSourceView| but of GTK+ and +governed by files such as ``settings.ini`` and ``gtk.css`` in +``$XDG_CONFIG_HOME/gtk-3.0`` or files in +``$HOME/.themes/NameOfTheme/gtk-3.0``, as well as the environment +variable ``GTK_THEME`` (search on internet for the various +possibilities). The fourth section is for customizing the editor. It includes in particular the ability to activate an Emacs mode named diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 921c7bbbf7..bc77e2e58c 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -245,9 +245,9 @@ file timing data: COQDEP Fast.v COQDEP Slow.v COQC Slow.v - Slow (user: 0.34 mem: 395448 ko) + Slow.vo (user: 0.34 mem: 395448 ko) COQC Fast.v - Fast (user: 0.01 mem: 45184 ko) + Fast.vo (user: 0.01 mem: 45184 ko) + ``pretty-timed`` this target stores the output of ``make TIMED=1`` into @@ -280,15 +280,15 @@ file timing data: COQDEP Fast.v COQDEP Slow.v COQC Slow.v - Slow (user: 0.36 mem: 393912 ko) + Slow.vo (user: 0.36 mem: 393912 ko) COQC Fast.v - Fast (user: 0.05 mem: 45992 ko) + Fast.vo (user: 0.05 mem: 45992 ko) Time | File Name -------------------- 0m00.41s | Total -------------------- - 0m00.36s | Slow - 0m00.05s | Fast + 0m00.36s | Slow.vo + 0m00.05s | Fast.vo + ``print-pretty-timed-diff`` @@ -338,8 +338,8 @@ file timing data: -------------------------------------------------------- 0m00.39s | Total | 0m00.35s || +0m00.03s | +11.42% -------------------------------------------------------- - 0m00.37s | Slow | 0m00.01s || +0m00.36s | +3600.00% - 0m00.02s | Fast | 0m00.34s || -0m00.32s | -94.11% + 0m00.37s | Slow.vo | 0m00.01s || +0m00.36s | +3600.00% + 0m00.02s | Fast.vo | 0m00.34s || -0m00.32s | -94.11% The following targets and ``Makefile`` variables allow collection of per- diff --git a/doc/sphinx/proof-engine/detailed-tactic-examples.rst b/doc/sphinx/proof-engine/detailed-tactic-examples.rst index 0ace9ef5b9..b63ae32311 100644 --- a/doc/sphinx/proof-engine/detailed-tactic-examples.rst +++ b/doc/sphinx/proof-engine/detailed-tactic-examples.rst @@ -353,7 +353,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in reset - Require Import Omega. + Require Import Lia. .. coqtop:: in @@ -367,7 +367,7 @@ the optional tactic of the ``Hint Rewrite`` command. .. coqtop:: in - Hint Rewrite g0 g1 g2 using omega : base1. + Hint Rewrite g0 g1 g2 using lia : base1. .. coqtop:: in diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 62708b01ed..1772362351 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -1715,6 +1715,7 @@ performance issue. .. coqtop:: reset in + Set Warnings "-omega-is-deprecated". Require Import Coq.omega.Omega. Ltac mytauto := tauto. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 90a991794f..28c5359a04 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -1624,9 +1624,15 @@ previous :token:`i_item` have been performed. The second entry in the :token:`i_view` grammar rule, ``/ltac:(`` :token:`tactic` ``)``, executes :token:`tactic`. -Notations can be used to name tactics, for example:: +Notations can be used to name tactics, for example - Notation myop := (ltac:(some ltac code)) : ssripat_scope. +.. coqtop:: none + + Tactic Notation "my" "ltac" "code" := idtac. + +.. coqtop:: in warn + + Notation "'myop'" := (ltac:(my ltac code)) : ssripat_scope. lets one write just ``/myop`` in the intro pattern. Note the scope annotation: views are interpreted opening the ``ssripat`` scope. @@ -2607,7 +2613,7 @@ After the :token:`i_pattern`, a list of binders is allowed. .. coqtop:: reset none From Coq Require Import ssreflect. - From Coq Require Import Omega. + From Coq Require Import ZArith Lia. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -2615,7 +2621,7 @@ After the :token:`i_pattern`, a list of binders is allowed. .. coqtop:: all Lemma test : True. - have H x (y : nat) : 2 * x + y = x + x + y by omega. + have H x (y : nat) : 2 * x + y = x + x + y by lia. A proof term provided after ``:=`` can mention these bound variables (that are automatically introduced with the given names). @@ -2625,7 +2631,7 @@ with parentheses even if no type is specified: .. coqtop:: all restart - have (x) : 2 * x = x + x by omega. + have (x) : 2 * x = x + x by lia. The :token:`i_item` and :token:`s_item` can be used to interpret the asserted hypothesis with views (see section :ref:`views_and_reflection_ssr`) or simplify the resulting @@ -2668,9 +2674,9 @@ context entry name. Arguments Sub {_} _ _. Lemma test n m (H : m + 1 < n) : True. - have @i : 'I_n by apply: (Sub m); omega. + have @i : 'I_n by apply: (Sub m); lia. -Note that the subterm produced by :tacn:`omega` is in general huge and +Note that the subterm produced by :tacn:`lia` is in general huge and uninteresting, and hence one may want to hide it. For this purpose the ``[: name ]`` intro pattern and the tactic ``abstract`` (see :ref:`abstract_ssr`) are provided. @@ -2680,7 +2686,7 @@ For this purpose the ``[: name ]`` intro pattern and the tactic .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. - have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; omega. + have [:pm] @i : 'I_n by apply: (Sub m); abstract: pm; lia. The type of ``pm`` can be cleaned up by its annotation ``(*1*)`` by just simplifying it. The annotations are there for technical reasons only. @@ -2694,7 +2700,7 @@ with have and an explicit term, they must be used as follows: Lemma test n m (H : m + 1 < n) : True. have [:pm] @i : 'I_n := Sub m pm. - by omega. + by lia. In this case the abstract constant ``pm`` is assigned by using it in the term that follows ``:=`` and its corresponding goal is left to be @@ -2712,7 +2718,7 @@ makes use of it). .. coqtop:: all abort Lemma test n m (H : m + 1 < n) : True. - have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; omega. + have [:pm] @i k : 'I_(n+k) by apply: (Sub m); abstract: pm k; lia. Last, notice that the use of intro patterns for abstract constants is orthogonal to the transparent flag ``@`` for have. @@ -2963,7 +2969,7 @@ illustrated in the following example. .. coqtop:: reset none - From Coq Require Import ssreflect Omega. + From Coq Require Import ssreflect Lia. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 6a280b74c2..7e6da490fb 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -1875,6 +1875,7 @@ analysis on inductive or co-inductive objects (see :ref:`inductive-definitions`) Lemma induction_test : forall n:nat, n = n -> n <= n. intros n H. induction n. + exact (le_n 0). .. exn:: Not an inductive product. :undocumented: @@ -2076,7 +2077,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 +2105,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 +2612,8 @@ and an explanation of the underlying technique. assumption. Qed. +.. seealso:: :tacn:`functional inversion` + .. tacn:: fix @ident @num :name: fix @@ -3134,8 +3076,10 @@ the conversion in hypotheses :n:`{+ @ident}`. .. flag:: NativeCompute Timing This flag causes all calls to the native compiler to print - timing information for the compilation, execution, and - reification phases of native compilation. + timing information for the conversion to native code, + compilation, execution, and reification phases of native + compilation. Timing is printed in units of seconds of + wall-clock time. .. flag:: NativeCompute Profiling @@ -4008,10 +3952,10 @@ At Coq startup, only the core database is nonempty and can be used. :arith: This database contains all lemmas about Peano’s arithmetic proved in the directories Init and Arith. -:zarith: contains lemmas about binary signed integers from the directories - theories/ZArith. When required, the module Omega also extends the - database zarith with a high-cost hint that calls ``omega`` on equations - and inequalities in ``nat`` or ``Z``. +:zarith: contains lemmas about binary signed integers from the + directories theories/ZArith. The database also contains + high-cost hints that call :tacn:`lia` on equations and + inequalities in ``nat`` or ``Z``. :bool: contains lemmas about booleans, mostly from directory theories/Bool. @@ -4602,42 +4546,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 ----------------- @@ -4694,18 +4602,6 @@ Automating The goal is not of the form :g:`t = u`. Especially note that :tacn:`btauto` doesn't introduce variables into the context on its own. -.. tacn:: omega - :name: omega - - The tactic :tacn:`omega`, due to Pierre Crégut, is an automatic decision - procedure for Presburger arithmetic. It solves quantifier-free - formulas built with `~`, `\\/`, `/\\`, `->` on top of equalities, - inequalities and disequalities on both the type :g:`nat` of natural numbers - and :g:`Z` of binary integers. This tactic must be loaded by the command - ``Require Import Omega``. See the additional documentation about omega - (see Chapter :ref:`omega`). - - .. tacn:: ring :name: ring 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/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/hidden-files b/doc/stdlib/hidden-files index 67d0b37e81..65c88ed8d5 100644 --- a/doc/stdlib/hidden-files +++ b/doc/stdlib/hidden-files @@ -44,6 +44,7 @@ theories/micromega/Refl.v theories/micromega/RingMicromega.v theories/micromega/Tauto.v theories/micromega/VarMap.v +theories/micromega/ZArith_hints.v theories/micromega/ZCoeff.v theories/micromega/ZMicromega.v theories/micromega/ZifyInst.v 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/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py index b448d0f9d3..57243207f0 100644 --- a/doc/tools/coqrst/coqdomain.py +++ b/doc/tools/coqrst/coqdomain.py @@ -188,20 +188,19 @@ class CoqObject(ObjectDescription): def _add_index_entry(self, name, target): """Add `name` (pointing to `target`) to the main index.""" assert isinstance(name, str) - if not name.startswith("_"): - # remove trailing . , found in commands, but not ... (ellipsis) - trim = name.endswith(".") and not name.endswith("...") - index_text = name[:-1] if trim else name - if self.index_suffix: - index_text += " " + self.index_suffix - self.indexnode['entries'].append(('single', index_text, target, '', None)) + # remove trailing . , found in commands, but not ... (ellipsis) + trim = name.endswith(".") and not name.endswith("...") + index_text = name[:-1] if trim else name + if self.index_suffix: + index_text += " " + self.index_suffix + self.indexnode['entries'].append(('single', index_text, target, '', None)) aliases = None # additional indexed names for a command or other object def add_target_and_index(self, name, _, signode): """Attach a link target to `signode` and an index entry for `name`. This is only called (from ``ObjectDescription.run``) if ``:noindex:`` isn't specified.""" - if name: + if name and not (isinstance(name, str) and name.startswith('_')): target = self._add_target(signode, name) self._add_index_entry(name, target) if self.aliases is not None: diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg index a01f57eb22..700170b3c6 100644 --- a/doc/tools/docgram/common.edit_mlg +++ b/doc/tools/docgram/common.edit_mlg @@ -511,6 +511,12 @@ strategy_flag: [ | OPTINREF ] +filtered_import: [ +| REPLACE global "(" LIST1 one_import_filter_name SEP "," ")" +| WITH global OPT [ "(" LIST1 one_import_filter_name SEP "," ")" ] +| DELETE global +] + functor_app_annot: [ | OPTINREF ] @@ -900,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 @@ -963,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 ] @@ -1544,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 @@ -1582,6 +1588,7 @@ SPLICE: [ | searchabout_queries | locatable | scope_delimiter +| one_import_filter_name ] (* end SPLICE *) RENAME: [ diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar index dc7e0fba37..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 @@ -1031,8 +1031,8 @@ gallina_ext: [ | "Collection" identref ":=" section_subset_expr | "Require" export_token LIST1 global | "From" global "Require" export_token LIST1 global -| "Import" LIST1 global -| "Export" LIST1 global +| "Import" LIST1 filtered_import +| "Export" LIST1 filtered_import | "Include" module_type_inl LIST0 ext_module_expr | "Include" "Type" module_type_inl LIST0 ext_module_type | "Transparent" LIST1 smart_global @@ -1057,6 +1057,15 @@ gallina_ext: [ | "Export" "Unset" option_table ] +filtered_import: [ +| global +| global "(" LIST1 one_import_filter_name SEP "," ")" +] + +one_import_filter_name: [ +| global OPT [ "(" ".." ")" ] +] + export_token: [ | "Import" | "Export" @@ -1309,7 +1318,7 @@ option_setting: [ | STRING ] -option_ref_value: [ +table_value: [ | global | STRING ] diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar index ac986f9adf..e71c80f829 100644 --- a/doc/tools/docgram/orderedGrammar +++ b/doc/tools/docgram/orderedGrammar @@ -497,6 +497,10 @@ constructor: [ | ident LIST0 binder OPT of_type ] +filtered_import: [ +| qualid OPT [ "(" LIST1 ( qualid OPT [ "(" ".." ")" ] ) SEP "," ")" ] +] + cofix_definition: [ | ident_decl LIST0 binder OPT ( ":" type ) OPT [ ":=" term ] OPT decl_notations ] @@ -849,8 +853,8 @@ command: [ | "Collection" ident ":=" section_subset_expr | "Require" OPT [ "Import" | "Export" ] LIST1 qualid | "From" dirpath "Require" OPT [ "Import" | "Export" ] LIST1 qualid -| "Import" LIST1 qualid -| "Export" LIST1 qualid +| "Import" LIST1 filtered_import +| "Export" LIST1 filtered_import | "Include" module_type_inl LIST0 ( "<+" module_expr_inl ) | "Include" "Type" LIST1 module_type_inl SEP "<+" | "Transparent" LIST1 smart_qualid |