From a75914f098a66bd628b162e6d9e8614451c9c8aa Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Mon, 14 May 2018 15:05:59 +0200 Subject: [sphinx] Fix mistake in index. --- doc/sphinx/proof-engine/tactics.rst | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- cgit v1.2.3