diff options
| author | coqbot-app[bot] | 2021-01-01 19:06:50 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-01 19:06:50 +0000 |
| commit | 66e24a2365b235bd35cbba71adce30dccea60b55 (patch) | |
| tree | 6af6efaaefddf7d3ce6a73d1899c421f566289ec /doc/sphinx/addendum/type-classes.rst | |
| parent | 6e18c48238edea6f69a2f96b58acd368bf8cc258 (diff) | |
| parent | e02120ed6580733db2276f0c11b4f432ea670ee3 (diff) | |
Merge PR #13470: Convert rewriting and proof-mode chapters to prodn
Reviewed-by: Zimmi48
Ack-by: JasonGross
Diffstat (limited to 'doc/sphinx/addendum/type-classes.rst')
| -rw-r--r-- | doc/sphinx/addendum/type-classes.rst | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index 4143d836c4..8dc0030115 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -160,7 +160,7 @@ Sections and contexts --------------------- To ease developments parameterized by many instances, one can use the -:cmd:`Context` command to introduce these parameters into section contexts, +:cmd:`Context` command to introduce the parameters into the :term:`local context`, it works similarly to the command :cmd:`Variable`, except it accepts any binding context as an argument, so variables can be implicit, and :ref:`implicit-generalization` can be used. @@ -422,7 +422,7 @@ Summary of the commands resolution with the local hypotheses use full conversion during unification. - + The mode hints (see :cmd:`Hint Mode`) associated to a class are + + The mode hints (see :cmd:`Hint Mode`) associated with a class are taken into account by :tacn:`typeclasses eauto`. When a goal does not match any of the declared modes for its head (if any), instead of failing like :tacn:`eauto`, the goal is suspended and @@ -470,7 +470,6 @@ Summary of the commands refinement engine will be able to backtrack. .. tacn:: autoapply @one_term with @ident - :name: autoapply The tactic ``autoapply`` applies :token:`one_term` using the transparency information of the hint database :token:`ident`, and does *no* typeclass resolution. This can @@ -590,7 +589,6 @@ Settings :cmd:`Typeclasses eauto` is another way to set this flag. .. opt:: Typeclasses Depth @natural - :name: Typeclasses Depth Sets the maximum proof search depth. The default is unbounded. :cmd:`Typeclasses eauto` is another way to set this option. @@ -602,7 +600,6 @@ Settings is another way to set this flag. .. opt:: Typeclasses Debug Verbosity @natural - :name: Typeclasses Debug Verbosity Determines how much information is shown for typeclass resolution steps during search. 1 is the default level. 2 shows additional information such as tried tactics and shelving @@ -613,7 +610,6 @@ Typeclasses eauto ~~~~~~~~~~~~~~~~~ .. cmd:: Typeclasses eauto := {? debug } {? ( {| bfs | dfs } ) } {? @natural } - :name: Typeclasses eauto Allows more global customization of the :tacn:`typeclasses eauto` tactic. The options are: |