diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst
index 96fda9925aec..56fe0e7208a1 100644
--- a/doc/sphinx/proof-engine/vernacular-commands.rst
+++ b/doc/sphinx/proof-engine/vernacular-commands.rst
@@ -70,13 +70,18 @@ described elsewhere
 
 .. cmd:: About @reference {? @univ_name_list }
 
-   Displays information about the :n:`@reference` object, which,
-   if a proof is open,  may be a hypothesis of the selected goal,
-   or an accessible theorem, axiom, etc.:
-   its kind (module, constant, assumption, inductive,
-   constructor, abbreviation, …), long name, type, implicit arguments and
+   Displays information about the :n:`@reference` object, which may be the
+   name of any accessible defined symbol, such as a theorem, constructor,
+   fixpoint or module.  If a proof is open, :n:`@reference` may refer to a
+   hypothesis of the selected goal.  The information includes:
+   the kind of the object (module, constant, assumption, inductive,
+   constructor, abbreviation, projection, coercion,  …), long name, type,
+   opacity/transparency, implicit arguments, argument names and
    argument scopes (as set in the definition of :token:`reference` or
-   subsequently with the :cmd:`Arguments` command). It does not print the body of definitions or proofs.
+   subsequently with the :cmd:`Arguments` command). It does not print the
+   body of definitions or proofs.
+
+   See :cmd:`Strategy` for details on opacity.
 
 .. cmd:: Check @term
 
diff --git a/doc/sphinx/proofs/writing-proofs/equality.rst b/doc/sphinx/proofs/writing-proofs/equality.rst
index 41802bed5773..9a16b7f2a393 100644
--- a/doc/sphinx/proofs/writing-proofs/equality.rst
+++ b/doc/sphinx/proofs/writing-proofs/equality.rst
@@ -996,6 +996,8 @@ which supports additional fine-tuning.
    constants always remain transparent. This mechanism is only intended for
    debugging purposes.
 
+   Use the :cmd:`About` command to see if a symbol is transparent or opaque.
+
 .. cmd:: Transparent {? ! } {+ @reference }
 
    The opposite of :cmd:`Opaque`, it marks the specified constants
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 2a9ab4e31fee..9ea7eaa9cf41 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -174,13 +174,13 @@ let print_opacity env ref =
         match s with
           | FullyOpaque -> str "opaque"
           | TransparentMaybeOpacified Conv_oracle.Opaque ->
-              str "basically transparent but considered opaque for reduction"
+              str "opaque but may be made transparent"
           | TransparentMaybeOpacified lev when Conv_oracle.is_transparent lev ->
               str "transparent"
           | TransparentMaybeOpacified (Conv_oracle.Level n) ->
-              str "transparent (with expansion weight " ++ int n ++ str ")"
+              str "transparent (level " ++ int n ++ str ")"
           | TransparentMaybeOpacified Conv_oracle.Expand ->
-              str "transparent (with minimal expansion weight)"]
+              str "transparent (expand)"]
 
 (** Printing coercion status *)