diff options
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 21 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 2 |
2 files changed, 17 insertions, 6 deletions
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 8dbe659606..67d32835f5 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3284,6 +3284,17 @@ the conversion in hypotheses :n:`{+ @ident}`. Goal 0 <= 1. unfold le. + This error can also be raised if you are trying to unfold + something that has been marked as opaque. + + .. example:: + + .. coqtop:: abort all fail + + Opaque Nat.add. + Goal 1 + 0 = 1. + unfold Nat.add. + .. tacv:: unfold @qualid in @goal_occurrences Replaces :n:`@qualid` in hypothesis (or hypotheses) designated @@ -3292,9 +3303,9 @@ the conversion in hypotheses :n:`{+ @ident}`. .. tacv:: unfold {+, @qualid} - Replaces *simultaneously* :n:`{+, @qualid}` with their - definitions and replaces the current goal with its - :math:`\beta`:math:`\iota` normal form. + Replaces :n:`{+, @qualid}` with their definitions and replaces + the current goal with its :math:`\beta`:math:`\iota` normal + form. .. tacv:: unfold {+, @qualid at @occurrences } @@ -3312,8 +3323,8 @@ the conversion in hypotheses :n:`{+ @ident}`. If :n:`@string` denotes the discriminating symbol of a notation (e.g. "+") or an expression defining a notation (e.g. `"_ + - _"`), and this notation refers to an unfoldable constant, then - the tactic unfolds it. + _"`), and this notation denotes an application whose head symbol + is an unfoldable constant, then the tactic unfolds it. .. tacv:: unfold @string%@ident diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index a436ae1651..5f3e82938d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -1175,7 +1175,7 @@ described first. particular declaring the same name in several modules or in several functor applications will be rejected if these declarations are not local. The name :n:`@ident` cannot be used directly as an Ltac tactic, but - nothing prevents the user to also perform a + nothing prevents the user from also performing a :n:`Ltac @ident := @redexpr`. .. seealso:: :ref:`performingcomputations` |