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/08-tools/12126-adjust-timed-name.rst8
-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/sphinx/practical-tools/utilities.rst16
-rw-r--r--doc/sphinx/proof-engine/vernacular-commands.rst24
-rw-r--r--doc/stdlib/index-list.html.template1
-rw-r--r--doc/tools/docgram/common.edit_mlg18
-rw-r--r--doc/tools/docgram/fullGrammar12
11 files changed, 94 insertions, 25 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/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/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/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/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 7d031b9b7a..a0d1080314 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.
diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template
index 7fa621c11c..b181951767 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
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-03 08:15:49 +0000