diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-14 15:05:59 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-16 17:10:16 +0200 |
| commit | a75914f098a66bd628b162e6d9e8614451c9c8aa (patch) | |
| tree | 429c2e36bdb3d144b78dd465de6eb49af077085f /doc/sphinx/proof-engine | |
| parent | f29a9c409272271260256792f64abf7475984e77 (diff) | |
[sphinx] Fix mistake in index.
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 a37107afd..da4c3f9d7 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3422,7 +3422,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is Adds each :n:`Hint Unfold @ident`. .. cmdv:: Hint %( Transparent %| Opaque %) @qualid - :name: Hint %( Transparent %| Opaque %) + :name: Hint ( Transparent | Opaque ) This adds a transparency hint to the database, making :n:`@qualid` a transparent or opaque constant during resolution. This information is used |