diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/practical-tools/utilities.rst | 8 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 14 |
2 files changed, 15 insertions, 7 deletions
diff --git a/doc/sphinx/practical-tools/utilities.rst b/doc/sphinx/practical-tools/utilities.rst index 35231610fe..554f6bf230 100644 --- a/doc/sphinx/practical-tools/utilities.rst +++ b/doc/sphinx/practical-tools/utilities.rst @@ -909,13 +909,15 @@ Command line options :--coqlib url: Set base URL for the Coq standard library (default is `<http://coq.inria.fr/library/>`_). This is equivalent to ``--external url Coq``. - :-R dir coqdir: Map physical directory dir to |Coq| logical + :-R dir coqdir: Recursively map physical directory dir to |Coq| logical directory ``coqdir`` (similarly to |Coq| option ``-R``). + :-Q dir coqdir: Map physical directory dir to |Coq| logical + directory ``coqdir`` (similarly to |Coq| option ``-Q``). .. note:: - option ``-R`` only has - effect on the files *following* it on the command line, so you will + options ``-R`` and ``-Q`` only have + effect on the files *following* them on the command line, so you will probably need to put this option first. diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 658ac857fb..0f78a9b84a 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3863,9 +3863,9 @@ The general command to add a hint to some databases :n:`{+ @ident}` is 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 + 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 + scrutinee’s head, recursively, casts being ignored. :cmd:`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 ``!`` @@ -3874,8 +3874,14 @@ The general command to add a hint to some databases :n:`{+ @ident}` is .. note:: - One can use an ``Extern`` hint with no pattern to do pattern matching on - hypotheses using ``match goal with`` inside the tactic. + + One can use a :cmd:`Hint Extern` with no pattern to do + pattern matching on hypotheses using ``match goal with`` + inside the tactic. + + + If you want to add hints such as :cmd:`Hint Transparent`, + :cmd:`Hint Cut`, or :cmd:`Hint Mode`, for typeclass + resolution, do not forget to put them in the + ``typeclass_instances`` hint database. Hint databases defined in the Coq standard library |