diff options
| author | Théo Zimmermann | 2018-12-11 19:27:46 +0100 |
|---|---|---|
| committer | Théo Zimmermann | 2018-12-11 19:27:46 +0100 |
| commit | b86196e9c643171c161a3a48ccabeea451481cbf (patch) | |
| tree | 5819dcec2e20bb256be1c29bef7d3ee17192c293 /doc/sphinx/proof-engine | |
| parent | 99292a2a45f93cc27899c1f2ff4cda38c852c0b6 (diff) | |
Add missing formatting.
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 5958aed215..59602581c7 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3425,7 +3425,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. cmdv:: Hint @hint_definition - No database name is given: the hint is registered in the core database. + No database name is given: the hint is registered in the ``core`` database. .. deprecated:: 8.10 |