Suggestions from review.

Co-authored-by: Jason Gross <jgross@mit.edu>

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`