diff options
| author | Théo Zimmermann | 2019-05-23 17:57:20 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-05-23 17:57:20 +0200 |
| commit | 28bf625cbac7dcf4a21907674b5bd30eb53e5e87 (patch) | |
| tree | 92f30f86f4e47d9b27fe03774139d0be0be9fbe6 | |
| parent | d63295c766b26c7b9aa7b814a7df75d75de8a058 (diff) | |
Suggestions from review.
Co-authored-by: Jason Gross <jgross@mit.edu>
| -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` |