diff options
| author | Théo Zimmermann | 2018-12-11 16:00:15 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-11 16:00:15 +0100 |
| commit | 99292a2a45f93cc27899c1f2ff4cda38c852c0b6 (patch) | |
| tree | bf1668d9ab5578e4f7dc131926a8b20a13fc4c59 | |
| parent | 10b07a187522b74bbcc9355d3ff9c4153f300706 (diff) | |
Document the deprecation of hint declaration withou database in refman.
Follow-up of #8987.
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index ad80cb62e1..5958aed215 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3427,6 +3427,8 @@ The general command to add a hint to some databases :n:`{+ @ident}` is No database name is given: the hint is registered in the core database. + .. deprecated:: 8.10 + .. cmdv:: Local Hint @hint_definition : {+ @ident} This is used to declare hints that must not be exported to the other modules |