diff options
| author | Clément Pit-Claudel | 2020-05-02 14:06:49 -0400 |
|---|---|---|
| committer | Clément Pit-Claudel | 2020-05-02 14:06:49 -0400 |
| commit | 16b2734e050d4c28d5da1a509cd2387cb8cebe6b (patch) | |
| tree | 30660874fbc98736f1e092b827eaf2a67256c960 /doc/changelog | |
| parent | f129326d545ae27d362132b279167d119894a992 (diff) | |
| parent | 90285ff50290a49d20d60ffc59725bf87c6acd14 (diff) | |
Merge PR #12172: Refactor first chapter: first step, the section on basics.
Ack-by: JasonGross
Ack-by: jfehrle
Diffstat (limited to 'doc/changelog')
| -rw-r--r-- | doc/changelog/07-commands-and-options/11665-cumulative-attr.rst | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst index b6a034941d..7b690da68d 100644 --- a/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst +++ b/doc/changelog/07-commands-and-options/11665-cumulative-attr.rst @@ -6,7 +6,6 @@ ``Private`` (`#11665 <https://github.com/coq/coq/pull/11665>`_, by Théo Zimmermann). -- **Changed:** - Legacy attributes can now be passed in any order. See - :ref:`gallina-attributes` (`#11665 - <https://github.com/coq/coq/pull/11665>`_, by Théo Zimmermann). +- **Changed:** :term:`Legacy attributes <attribute>` can now be passed + in any order (`#11665 <https://github.com/coq/coq/pull/11665>`_, by + Théo Zimmermann). |