[sphinx] Improve part about Hints.

Fix Hint (Transparent | Opaque) index.

1 files changed, 112 insertions, 108 deletions

diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 8f4cbaf35..459c8500d 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -151,8 +151,8 @@ no numbers are given, all occurrences of :n:`@term` in the goal are selected.
 Finally, the last notation is an abbreviation for ``* |- *``. Note also
 that ``|-`` is optional in the first case when no ``*`` is given.
 
-Here are some tactics that understand occurrences clauses: ``set``, ``remember``
-, ``induction``, ``destruct``.
+Here are some tactics that understand occurrences clauses: :tacn:`set`, :tacn:`remember`
+, :tacn:`induction`, :tacn:`destruct`.
 
 
 See also: :ref:`Managingthelocalcontext`,
@@ -3290,39 +3290,41 @@ The hints databases for auto and eauto
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The hints for :tacn:`auto` and :tacn:`eauto` are stored in databases. Each database
-maps head symbols to a list of hints. One can use the command
+maps head symbols to a list of hints.
 
 .. cmd:: Print Hint @ident
 
-to display the hints associated to the head symbol :n:`@ident`
-(see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative
-integer, and an optional pattern. The hints with lower cost are tried first. A
-hint is tried by ``auto`` when the conclusion of the current goal matches its
-pattern or when it has no pattern.
+   Use this command
+   to display the hints associated to the head symbol :n:`@ident`
+   (see :ref:`Print Hint <printhint>`). Each hint has a cost that is a nonnegative
+   integer, and an optional pattern. The hints with lower cost are tried first. A
+   hint is tried by :tacn:`auto` when the conclusion of the current goal matches its
+   pattern or when it has no pattern.
 
 Creating Hint databases
 ```````````````````````
 
-One can optionally declare a hint database using the command ``Create
-HintDb``. If a hint is added to an unknown database, it will be
+One can optionally declare a hint database using the command
+:cmd:`Create HintDb`. If a hint is added to an unknown database, it will be
 automatically created.
 
 .. cmd:: Create HintDb @ident {? discriminated}
 
-This command creates a new database named :n:`@ident`. The database is
-implemented by a Discrimination Tree (DT) that serves as an index of
-all the lemmas. The DT can use transparency information to decide if a
-constant should be indexed or not (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`),
-making the retrieval more efficient. The legacy implementation (the default one
-for new databases) uses the DT only on goals without existentials (i.e., ``auto``
-goals), for non-Immediate hints and do not make use of transparency
-hints, putting more work on the unification that is run after
-retrieval (it keeps a list of the lemmas in case the DT is not used).
-The new implementation enabled by the discriminated option makes use
-of DTs in all cases and takes transparency information into account.
-However, the order in which hints are retrieved from the DT may differ
-from the order in which they were inserted, making this implementation
-observationally different from the legacy one.
+   This command creates a new database named :n:`@ident`. The database is
+   implemented by a Discrimination Tree (DT) that serves as an index of
+   all the lemmas. The DT can use transparency information to decide if a
+   constant should be indexed or not
+   (c.f. :ref:`The hints databases for auto and eauto <thehintsdatabasesforautoandeauto>`),
+   making the retrieval more efficient. The legacy implementation (the default one
+   for new databases) uses the DT only on goals without existentials (i.e., :tacn:`auto`
+   goals), for non-Immediate hints and do not make use of transparency
+   hints, putting more work on the unification that is run after
+   retrieval (it keeps a list of the lemmas in case the DT is not used).
+   The new implementation enabled by the discriminated option makes use
+   of DTs in all cases and takes transparency information into account.
+   However, the order in which hints are retrieved from the DT may differ
+   from the order in which they were inserted, making this implementation
+   observationally different from the legacy one.
 
 The general command to add a hint to some databases :n:`{+ @ident}` is
 
@@ -3346,21 +3348,21 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
    .. cmdv:: Hint Resolve @term {? | {? @num} {? @pattern}}
       :name: Hint Resolve
 
-   This command adds :n:`simple apply @term` to the hint list with the head
-   symbol of the type of :n:`@term`. The cost of that hint is the number of
-   subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The
-   associated :n:`@pattern` is inferred from the conclusion of the type of
-   :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type
-   of :n:`@term` does not start with a product the tactic added in the hint list
-   is :n:`exact @term`. In case this type can however be reduced to a type
-   starting with a product, the tactic :n:`simple apply @term` is also stored in
-   the hints list. If the inferred type of :n:`@term` contains a dependent
-   quantification on a variable which occurs only in the premisses of the type
-   and not in its conclusion, no instance could be inferred for the variable by
-   unification with the goal. In this case, the hint is added to the hint list
-   of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A
-   typical example of a hint that is used only by :tacn:`eauto` is a transitivity
-   lemma.
+      This command adds :n:`simple apply @term` to the hint list with the head
+      symbol of the type of :n:`@term`. The cost of that hint is the number of
+      subgoals generated by :n:`simple apply @term` or :n:`@num` if specified. The
+      associated :n:`@pattern` is inferred from the conclusion of the type of
+      :n:`@term` or the given :n:`@pattern` if specified. In case the inferred type
+      of :n:`@term` does not start with a product the tactic added in the hint list
+      is :n:`exact @term`. In case this type can however be reduced to a type
+      starting with a product, the tactic :n:`simple apply @term` is also stored in
+      the hints list. If the inferred type of :n:`@term` contains a dependent
+      quantification on a variable which occurs only in the premisses of the type
+      and not in its conclusion, no instance could be inferred for the variable by
+      unification with the goal. In this case, the hint is added to the hint list
+      of :tacn:`eauto` instead of the hint list of auto and a warning is printed. A
+      typical example of a hint that is used only by :tacn:`eauto` is a transitivity
+      lemma.
 
    .. exn:: @term cannot be used as a hint
 
@@ -3388,7 +3390,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       This command adds :n:`simple apply @term; trivial` to the hint list associated
       with the head symbol of the type of :n:`@ident` in the given database. This
       tactic will fail if all the subgoals generated by :n:`simple apply @term` are
-      not solved immediately by the ``trivial`` tactic (which only tries tactics
+      not solved immediately by the :tacn:`trivial` tactic (which only tries tactics
       with cost 0).This command is useful for theorems such as the symmetry of
       equality or :g:`n+1=m+1 -> n=m` that we may like to introduce with a limited
       use in order to avoid useless proof-search. The cost of this tactic (which
@@ -3426,7 +3428,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
@@ -3434,52 +3436,54 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
       discrimination network to relax or constrain it in the case of discriminated
       databases.
 
-    .. cmdv:: Hint %(Transparent | Opaque) {+ @ident}
+   .. cmdv:: Hint %( Transparent %| Opaque %) {+ @ident}
 
       Declares each :n:`@ident` as a transparent or opaque constant.
 
-    .. cmdv:: Hint Extern @num {? @pattern} => tactic
+   .. cmdv:: Hint Extern @num {? @pattern} => tactic
 
-       This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
-       :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a
-       :n:`@tactic` to execute.
+      This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
+      :tacn:`unfold`. For that, we must specify a cost, an optional :n:`@pattern` and a
+      :n:`@tactic` to execute.
 
-       .. example::
+      .. example::
 
-          .. coqtop:: in
+         .. coqtop:: in
 
-             Hint Extern 4 (~(_ = _)) => discriminate.
+            Hint Extern 4 (~(_ = _)) => discriminate.
 
-       Now, when the head of the goal is a disequality, ``auto`` will try
-       discriminate if it does not manage to solve the goal with hints with a
-       cost less than 4. One can even use some sub-patterns of the pattern in
-       the tactic script. A sub-pattern is a question mark followed by an
-       identifier, like ``?X1`` or ``?X2``. Here is an example:
+         Now, when the head of the goal is a disequality, ``auto`` will try
+         discriminate if it does not manage to solve the goal with hints with a
+         cost less than 4.
 
-       .. example::
+      One can even use some sub-patterns of the pattern in
+      the tactic script. A sub-pattern is a question mark followed by an
+      identifier, like ``?X1`` or ``?X2``. Here is an example:
 
-          .. coqtop:: reset all
+      .. example::
 
-             Require Import List.
-             Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize  X1, X2; decide equality : eqdec.
-             Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
-             Info 1 auto with eqdec.
+         .. coqtop:: reset all
 
-    .. cmdv:: Hint Cut @regexp
+            Require Import List.
+            Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) => generalize  X1, X2; decide equality : eqdec.
+            Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
+            Info 1 auto with eqdec.
 
-       .. warning::
+   .. cmdv:: Hint Cut @regexp
 
-          These hints currently only apply to typeclass proof search and the
-          :tacn:`typeclasses eauto` tactic.
+      .. warning::
 
-       This command can be used to cut the proof-search tree according to a regular
-       expression matching paths to be cut. The grammar for regular expressions is
-       the following. Beware, there is no operator precedence during parsing, one can
-       check with :cmd:`Print HintDb` to verify the current cut expression:
+         These hints currently only apply to typeclass proof search and the
+         :tacn:`typeclasses eauto` tactic.
 
-       .. productionlist:: `regexp`
+      This command can be used to cut the proof-search tree according to a regular
+      expression matching paths to be cut. The grammar for regular expressions is
+      the following. Beware, there is no operator precedence during parsing, one can
+      check with :cmd:`Print HintDb` to verify the current cut expression:
+
+      .. productionlist:: `regexp`
           e : ident      hint or instance identifier
-            :|_         any hint
+            :| _         any hint
             :| e\|e′     disjunction
             :| e e′      sequence
             :| e *       Kleene star
@@ -3487,42 +3491,42 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
             :| eps       epsilon
             :| ( e  )
 
-       The `emp` regexp does not match any search path while `eps`
-       matches the empty path. During proof search, the path of
-       successive successful hints on a search branch is recorded, as a
-       list of identifiers for the hints (note Hint Extern’s do not have
-       an associated identifier).
-       Before applying any hint :n:`@ident` the current path `p` extended with
-       :n:`@ident` is matched against the current cut expression `c` associated to
-       the hint database. If matching succeeds, the hint is *not* applied. The
-       semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the
-       initial cut expression being `emp`.
-
-    .. cmdv:: Hint Mode @qualid {* (+ | ! | -)}
-
-       This sets an optional mode of use of the identifier :n:`@qualid`. When
-       proof-search faces a goal that ends in an application of :n:`@qualid` to
-       arguments :n:`@term ... @term`, the mode tells if the hints associated to
-       :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``,
-       ``!`` or ``-`` items that specify if an argument of the identifier is to be
-       treated as an input (``+``), if its head only is an input (``!``) or an output
-       (``-``) of the identifier. For a mode to match a list of arguments, input
-       terms and input heads *must not* contain existential variables or be
-       existential variables respectively, while outputs can be any term. Multiple
-       modes can be declared for a single identifier, in that case only one mode
-       needs to match the arguments for the hints to be applied.The head of a term
-       is understood here as the applicative head, or the match or projection
-       scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is
-       especially useful for typeclasses, when one does not want to support default
-       instances and avoid ambiguity in general. Setting a parameter of a class as an
-       input forces proof-search to be driven by that index of the class, with ``!``
-       giving more flexibility by allowing existentials to still appear deeper in the
-       index but not at its head.
-
-    .. note::
-
-       One can use an ``Extern`` hint with no pattern to do pattern-matching on
-       hypotheses using ``match goal`` with inside the tactic.
+      The `emp` regexp does not match any search path while `eps`
+      matches the empty path. During proof search, the path of
+      successive successful hints on a search branch is recorded, as a
+      list of identifiers for the hints (note Hint Extern’s do not have
+      an associated identifier).
+      Before applying any hint :n:`@ident` the current path `p` extended with
+      :n:`@ident` is matched against the current cut expression `c` associated to
+      the hint database. If matching succeeds, the hint is *not* applied. The
+      semantics of ``Hint Cut e`` is to set the cut expression to ``c | e``, the
+      initial cut expression being `emp`.
+
+   .. cmdv:: Hint Mode @qualid {* (+ | ! | -)}
+
+      This sets an optional mode of use of the identifier :n:`@qualid`. When
+      proof-search faces a goal that ends in an application of :n:`@qualid` to
+      arguments :n:`@term ... @term`, the mode tells if the hints associated to
+      :n:`@qualid` can be applied or not. A mode specification is a list of n ``+``,
+      ``!`` or ``-`` items that specify if an argument of the identifier is to be
+      treated as an input (``+``), if its head only is an input (``!``) or an output
+      (``-``) of the identifier. For a mode to match a list of arguments, input
+      terms and input heads *must not* contain existential variables or be
+      existential variables respectively, while outputs can be any term. Multiple
+      modes can be declared for a single identifier, in that case only one mode
+      needs to match the arguments for the hints to be applied.The head of a term
+      is understood here as the applicative head, or the match or projection
+      scrutinee’s head, recursively, casts being ignored. ``Hint Mode`` is
+      especially useful for typeclasses, when one does not want to support default
+      instances and avoid ambiguity in general. Setting a parameter of a class as an
+      input forces proof-search to be driven by that index of the class, with ``!``
+      giving more flexibility by allowing existentials to still appear deeper in the
+      index but not at its head.
+
+   .. note::
+
+      One can use an ``Extern`` hint with no pattern to do pattern-matching on
+      hypotheses using ``match goal`` with inside the tactic.
 
 
 Hint databases defined in the Coq standard library
@@ -3644,7 +3648,7 @@ described above: either they disappear at the end of a section scope,
 or they remain global forever. This causes a scalability issue,
 because hints coming from an unrelated part of the code may badly
 influence another development. It can be mitigated to some extent
-thanks to the ``Remove Hints`` command (see :ref:`Remove Hints <removehints>`),
+thanks to the :cmd:`Remove Hints` command,
 but this is a mere workaround and has some limitations (for instance, external
 hints cannot be removed).
 
@@ -3652,7 +3656,7 @@ A proper way to fix this issue is to bind the hints to their module scope, as
 for most of the other objects Coq uses. Hints should only made available when
 the module they are defined in is imported, not just required. It is very
 difficult to change the historical behavior, as it would break a lot of scripts.
-We propose a smooth transitional path by providing the ``Loose Hint Behavior``
+We propose a smooth transitional path by providing the :opt:`Loose Hint Behavior`
 option which accepts three flags allowing for a fine-grained handling of
 non-imported hints.