diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 56df535d85..1e17a773a6 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -35,7 +35,7 @@ Displaying .. cmdv:: Print {? Term } @qualid\@@name This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the raw universe is printed. + An underscore means the usual name is printed. .. cmd:: About @qualid @@ -49,7 +49,7 @@ Displaying .. cmdv:: About @qualid\@@name This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the raw universe is printed. + An underscore means the usual name is printed. .. cmd:: Print All |