diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac2.rst | 6 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 37 |
2 files changed, 34 insertions, 9 deletions
diff --git a/doc/sphinx/proof-engine/ltac2.rst b/doc/sphinx/proof-engine/ltac2.rst index cfdc70d50e..dd80b29bda 100644 --- a/doc/sphinx/proof-engine/ltac2.rst +++ b/doc/sphinx/proof-engine/ltac2.rst @@ -1,12 +1,12 @@ .. _ltac2: +Ltac2 +===== + .. coqtop:: none From Ltac2 Require Import Ltac2. -Ltac2 -===== - The Ltac tactic language is probably one of the ingredients of the success of Coq, yet it is at the same time its Achilles' heel. Indeed, Ltac: diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 81e50c0834..53cfb973d4 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 @@ -685,6 +688,28 @@ Applying theorems instantiate (see :ref:`Existential-Variables`). The instantiation is intended to be found later in the proof. + .. tacv:: rapply @term + :name: rapply + + The tactic :tacn:`rapply` behaves like :tacn:`eapply` but it + uses the proof engine of :tacn:`refine` for dealing with + existential variables, holes, and conversion problems. This may + result in slightly different behavior regarding which conversion + problems are solvable. However, like :tacn:`apply` but unlike + :tacn:`eapply`, :tacn:`rapply` will fail if there are any holes + which remain in :n:`@term` itself after typechecking and + typeclass resolution but before unification with the goal. More + technically, :n:`@term` is first parsed as a + :production:`constr` rather than as a :production:`uconstr` or + :production:`open_constr` before being applied to the goal. Note + that :tacn:`rapply` prefers to instantiate as many hypotheses of + :n:`@term` as possible. As a result, if it is possible to apply + :n:`@term` to arbitrarily many arguments without getting a type + error, :tacn:`rapply` will loop. + + Note that you need to :n:`Require Import Coq.Program.Tactics` to + make use of :tacn:`rapply`. + .. tacv:: simple apply @term. This behaves like :tacn:`apply` but it reasons modulo conversion only on subterms |