diff options
Diffstat (limited to 'doc/sphinx')
| -rw-r--r-- | doc/sphinx/dune | 8 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 15 |
2 files changed, 14 insertions, 9 deletions
diff --git a/doc/sphinx/dune b/doc/sphinx/dune index 353d58c676..b788fbbeed 100644 --- a/doc/sphinx/dune +++ b/doc/sphinx/dune @@ -1,8 +1,10 @@ (dirs :standard _static) -(rule (targets README.gen.rst) +(rule + (targets README.gen.rst) (deps (source_tree ../tools/coqrst) README.template.rst) (action (run ../tools/coqrst/regen_readme.py %{targets}))) -(alias (name refman-html) - (action (diff README.rst README.gen.rst))) +(rule + (alias refman-html) + (action (diff README.rst README.gen.rst))) diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 81e50c0834..878118c48a 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -555,12 +555,14 @@ Applying theorems This tactic applies to any goal. It behaves like :tacn:`exact` with a big difference: the user can leave some holes (denoted by ``_`` or :n:`(_ : @type)`) in the term. :tacn:`refine` will generate as many - subgoals as there are holes in the term. The type of holes must be either - synthesized by the system or declared by an explicit cast + subgoals as there are remaining holes in the elaborated term. The type + of holes must be either synthesized by the system or declared by an explicit cast like ``(_ : nat -> Prop)``. Any subgoal that occurs in other subgoals is automatically shelved, as if calling - :tacn:`shelve_unifiable`. This low-level tactic can be - useful to advanced users. + :tacn:`shelve_unifiable`. The produced subgoals (shelved or not) + are *not* candidates for typeclass resolution, even if they have a type-class + type as conclusion, letting the user control when and how typeclass resolution + is launched on them. This low-level tactic can be useful to advanced users. .. example:: @@ -611,8 +613,9 @@ Applying theorems .. tacv:: simple notypeclasses refine @term :name: simple notypeclasses refine - This tactic behaves like :tacn:`simple refine` except it performs type checking - without resolution of typeclasses. + This tactic behaves like the combination of :tacn:`simple refine` and + :tacn:`notypeclasses refine`: it performs type checking without resolution of + typeclasses, does not perform beta reductions or shelve the subgoals. .. flag:: Debug Unification |