diff options
| author | Théo Zimmermann | 2019-08-16 13:34:55 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-08-16 13:34:55 +0200 |
| commit | af4f14b16f8fc6817a2995b41398fdbbce1f74c9 (patch) | |
| tree | 4d8e3e2207ddfacf4ca62b3667b2c4c4699b9947 /doc | |
| parent | b8477fb38842016c226ba9d7be8f60486411a2ee (diff) | |
Fix quoting in 8.9 changelog entry.
Diffstat (limited to 'doc')
| -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 |