diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ltac.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 44 |
2 files changed, 26 insertions, 20 deletions
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst index 2b128b98fe..88c1e225fd 100644 --- a/doc/sphinx/proof-engine/ltac.rst +++ b/doc/sphinx/proof-engine/ltac.rst @@ -178,7 +178,7 @@ Sequence A sequence is an expression of the following form: .. tacn:: @expr ; @expr - :name: ; + :name: ltac-seq The expression :n:`@expr__1` is evaluated to :n:`v__1`, which must be a tactic value. The tactic :n:`v__1` is applied to the current goal, diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index da4c3f9d74..90ca0da432 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -879,14 +879,6 @@ quantification or an implication. This is equivalent to :n:`clear @ident. ... clear @ident.` -.. tacv:: clearbody @ident - :name: clearbody - - This tactic expects :n:`@ident` to be a local definition then clears its - body. Otherwise said, this tactic turns a definition into an assumption. - -.. exn:: @ident is not a local definition. - .. tacv:: clear - {+ @ident} This tactic clears all the hypotheses except the ones depending in the @@ -901,6 +893,15 @@ quantification or an implication. This clears the hypothesis :n:`@ident` and all the hypotheses that depend on it. +.. tacv:: clearbody {+ @ident} + :name: clearbody + + This tactic expects :n:`{+ @ident}` to be local definitions and clears their + respective bodies. + In other words, it turns the given definitions into assumptions. + +.. exn:: @ident is not a local definition. + .. tacn:: revert {+ @ident} :name: revert @@ -2867,8 +2868,8 @@ the conversion in hypotheses :n:`{+ @ident}`. .. coqtop:: all Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). - Notation "f \o g" := (fcomp f g) (at level 50). Arguments fcomp {A B C} f g x /. + Notation "f \o g" := (fcomp f g) (at level 50). After that command the expression :g:`(f \o g)` is left untouched by ``simpl`` while :g:`((f \o g) t)` is reduced to :g:`(f (g t))`. @@ -3702,19 +3703,24 @@ Setting implicit automation tactics time the term argument of a tactic has one of its holes not fully resolved. - .. example:: + .. deprecated:: 8.9 - .. coqtop:: all + This command is deprecated. Use :ref:`typeclasses <typeclasses>` or + :ref:`tactics-in-terms <tactics-in-terms>` instead. - Parameter quo : nat -> forall n:nat, n<>0 -> nat. - Notation "x // y" := (quo x y _) (at level 40). - Declare Implicit Tactic assumption. - Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. - intros. - exists (n // m). + .. example:: + + .. coqtop:: all + + Parameter quo : nat -> forall n:nat, n<>0 -> nat. + Notation "x // y" := (quo x y _) (at level 40). + Declare Implicit Tactic assumption. + Goal forall n m, m<>0 -> { q:nat & { r | q * m + r = n } }. + intros. + exists (n // m). - The tactic ``exists (n // m)`` did not fail. The hole was solved - by ``assumption`` so that it behaved as ``exists (quo n m H)``. + The tactic ``exists (n // m)`` did not fail. The hole was solved + by ``assumption`` so that it behaved as ``exists (quo n m H)``. .. _decisionprocedures: |