diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst | 6 | ||||
| -rw-r--r-- | doc/changelog/08-tools/12772-fix-details.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 2 |
3 files changed, 12 insertions, 1 deletions
diff --git a/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst b/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst new file mode 100644 index 0000000000..a05829b720 --- /dev/null +++ b/doc/changelog/08-tools/12754-master+fix-coqdoc-index-escaping.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Special symbols now escaped in the index produced by coqdoc, + avoiding collision with the syntax of the output format + (`#12754 <https://github.com/coq/coq/pull/12754>`_, + fixes `#12752 <https://github.com/coq/coq/issues/12752>`_, + by Hugo Herbelin). diff --git a/doc/changelog/08-tools/12772-fix-details.rst b/doc/changelog/08-tools/12772-fix-details.rst new file mode 100644 index 0000000000..67ee061285 --- /dev/null +++ b/doc/changelog/08-tools/12772-fix-details.rst @@ -0,0 +1,5 @@ +- **Fixed:** + The `details` environment added in the 8.12 release can now be used + as advertised in the reference manual + (`#12772 <https://github.com/coq/coq/pull/12772>`_, + by Thomas Letan). diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index 7b3670164b..3b4b80ca21 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -2280,7 +2280,7 @@ to the others. Iteration ~~~~~~~~~ -.. tacn:: do {? @num } {| @tactic | [ {+| @tactic } ] } +.. tacn:: do {? @mult } {| @tactic | [ {+| @tactic } ] } :name: do (ssreflect) This tactical offers an accurate control on the repetition of tactics. |