diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/03-notations/13842-remove-decimal.rst | 3 | ||||
| -rw-r--r-- | doc/changelog/04-tactics/13882-fix-ssr-setoidrw-in-hyp.rst | 6 | ||||
| -rw-r--r-- | doc/changelog/05-tactic-language/13236-ltac2-printf.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/changes.rst | 4 | ||||
| -rw-r--r-- | doc/sphinx/user-extensions/syntax-extensions.rst | 6 | ||||
| -rw-r--r-- | doc/stdlib/index-list.html.template | 1 |
6 files changed, 19 insertions, 8 deletions
diff --git a/doc/changelog/03-notations/13842-remove-decimal.rst b/doc/changelog/03-notations/13842-remove-decimal.rst new file mode 100644 index 0000000000..4bc26ef6a8 --- /dev/null +++ b/doc/changelog/03-notations/13842-remove-decimal.rst @@ -0,0 +1,3 @@ +- **Removed:** + Remove decimal-only number notations which were deprecated in 8.12. + (`#13842 <https://github.com/coq/coq/pull/13842>`_, by Pierre Roux). diff --git a/doc/changelog/04-tactics/13882-fix-ssr-setoidrw-in-hyp.rst b/doc/changelog/04-tactics/13882-fix-ssr-setoidrw-in-hyp.rst new file mode 100644 index 0000000000..31b331f0ff --- /dev/null +++ b/doc/changelog/04-tactics/13882-fix-ssr-setoidrw-in-hyp.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Setoid rewriting now remembers the (invisible) binder names of non-dependent product types. SSReflect's rewrite tactic expects these names to be retained when using ``rewrite foo in H``. + This also fixes SSR ``rewrite foo in H *`` erroneously reverting ``H``. + (`#13882 <https://github.com/coq/coq/pull/13882>`_, + fixes `#12011 <https://github.com/coq/coq/issues/12011>`_, + by Gaëtan Gilbert). diff --git a/doc/changelog/05-tactic-language/13236-ltac2-printf.rst b/doc/changelog/05-tactic-language/13236-ltac2-printf.rst new file mode 100644 index 0000000000..02213f22e5 --- /dev/null +++ b/doc/changelog/05-tactic-language/13236-ltac2-printf.rst @@ -0,0 +1,7 @@ +- **Added:** + Added a ``printf`` macro to Ltac2. It can be made accessible by + importing the ``Ltac2.Printf`` module. See the documentation + there for more information + (`#13236 <https://github.com/coq/coq/pull/13236>`_, + fixes `#10108 <https://github.com/coq/coq/issues/10108>`_, + by Pierre-Marie Pédrot). diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index ea099eb52e..8fa1b97851 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -82,13 +82,13 @@ Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Arnaud Spiwack, Matthieu Sozeau, Enrico Tassi, Laurent Théry, Anton Trunov, Li-yao Xia and Théo Zimmermann. -The 52 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric +The 51 contributors to this version are Reynald Affeldt, Tanaka Akira, Frédéric Besson, Lasse Blaauwbroek, Clément Blaudeau, Martin Bodin, Ali Caglayan, Tej Chajed, Cyril Cohen, Julien Coolen, Matthew Dempsky, Maxime Dénès, Andres Erbsen, Jim Fehrle, Emilio Jesús Gallego Arias, Paolo G. Giarrusso, Attila Gáspár, Gaëtan Gilbert, Jason Gross, Benjamin Grégoire, Hugo Herbelin, Wolf Honore, Jasper Hugunin, Ignat Insarov, Ralf Jung, Fabian Kunze, Vincent Laporte, Olivier Laurent, Larry D. Lee Jr, -Thomas Letan, Yishuai Li, Xia Li-yao, James Lottes, Jean-Christophe Léchenet, +Thomas Letan, Yishuai Li, James Lottes, Jean-Christophe Léchenet, Kenji Maillard, Erik Martin-Dorel, Yusuke Matsushita, Guillaume Melquiond, Carl Patenaude-Poulin, Clément Pit-Claudel, Pierre-Marie Pédrot, Pierre Roux, Kazuhiko Sakaguchi, Vincent Semeria, Michael Soegtrop, Matthieu Sozeau, diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 03571ad680..557ef10555 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -1726,12 +1726,6 @@ Number notations * :n:`@qualid__type -> Number.number` * :n:`@qualid__type -> option Number.number` - .. deprecated:: 8.12 - Number notations on :g:`Decimal.uint`, :g:`Decimal.int` and - :g:`Decimal.decimal` are replaced respectively by number - notations on :g:`Number.uint`, :g:`Number.int` and - :g:`Number.number`. - When parsing, the application of the parsing function :n:`@qualid__parse` to the number will be fully reduced, and universes of the resulting term will be refreshed. diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index 27eb64a83b..b0f4e883be 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -692,6 +692,7 @@ through the <tt>Require Import</tt> command.</p> user-contrib/Ltac2/Notations.v user-contrib/Ltac2/Option.v user-contrib/Ltac2/Pattern.v + user-contrib/Ltac2/Printf.v user-contrib/Ltac2/Std.v user-contrib/Ltac2/String.v </dd> |