diff options
| author | Clément Pit-Claudel | 2019-08-16 19:35:32 +0200 |
|---|---|---|
| committer | Clément Pit-Claudel | 2019-08-16 19:35:32 +0200 |
| commit | 354ac6a0c59f77d8a7d63c84144c044fe958fa3c (patch) | |
| tree | 85b91c9c27509784e0ce2b528db347ae03775816 | |
| parent | d72acd6f1a5abb8066b6922e5e972fa17b215591 (diff) | |
| parent | af4f14b16f8fc6817a2995b41398fdbbce1f74c9 (diff) | |
Merge PR #10663: Fix quoting in 8.9 changelog entry.
Reviewed-by: cpitclaudel
| -rw-r--r-- | doc/sphinx/changes.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/changes.rst b/doc/sphinx/changes.rst index 6ac55e7bf4..c591a1f1de 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -894,8 +894,8 @@ Standard Library and other packages. They are still delimited by `%int` and `%uint`. - Syntax notations for `string`, `ascii`, `Z`, `positive`, `N`, `R`, - and `int31` are no longer available merely by `Require`ing the files - that define the inductives. You must `Import` `Coq.Strings.String.StringSyntax` + and `int31` are no longer available merely by :cmd:`Require`\ing the files + that define the inductives. You must :cmd:`Import` `Coq.Strings.String.StringSyntax` (after `Require` `Coq.Strings.String`), `Coq.Strings.Ascii.AsciiSyntax` (after `Require` `Coq.Strings.Ascii`), `Coq.ZArith.BinIntDef`, `Coq.PArith.BinPosDef`, `Coq.NArith.BinNatDef`, `Coq.Reals.Rdefinitions`, and |