diff options
| author | Théo Zimmermann | 2020-03-18 18:36:10 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2020-03-19 18:05:03 +0100 |
| commit | 2c785aaab9b54b3d3406e7e021de635247f6535c (patch) | |
| tree | 471d63dbd0926c60eca90466bbdf73e0537ed07b /doc/sphinx/changes.rst | |
| parent | 9f834bd7ca7de79dfb2d9f9633ac93464ab1342d (diff) | |
Document all the existing attributes.
And fix documentation following the removal of the Template Check flag
in #11546.
Diffstat (limited to 'doc/sphinx/changes.rst')
| -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 6d9979a704..8855b54f5b 100644 --- a/doc/sphinx/changes.rst +++ b/doc/sphinx/changes.rst @@ -220,7 +220,7 @@ Changes in 8.11+beta1 .. _811RefineInstance: -- **Added:** ``#[refine]`` attribute for :cmd:`Instance`, a more +- **Added:** :attr:`refine` attribute for :cmd:`Instance`, a more predictable version of the old ``Refine Instance Mode`` which unconditionally opens a proof (`#10996 <https://github.com/coq/coq/pull/10996>`_, by Gaëtan Gilbert). @@ -1314,7 +1314,7 @@ Changes in 8.10+beta3 rules governing template-polymorphic types. To help users incrementally fix this issue, a command line option - `-no-template-check` and a global flag :flag:`Template Check` are + `-no-template-check` and a global flag ``Template Check`` are available to selectively disable the new check. Use at your own risk. (`#9918 <https://github.com/coq/coq/pull/9918>`_, by Matthieu Sozeau |