diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-24 11:59:50 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-05 11:54:03 +0200 |
| commit | bd16a458b71952073ac1ad1525bafe35aea56a5b (patch) | |
| tree | c87fb39f0ab295b4fb04b5e6aae87ad8fc957ba9 | |
| parent | 1ed5cc920523fc8e7ea61bb3962b235a310dfa71 (diff) | |
[sphinx] Use references for Print.
| -rw-r--r-- | doc/sphinx/proof-engine/vernacular-commands.rst | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 0d160a025..d8bf9582d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -15,6 +15,7 @@ Displaying .. _Print: .. cmd:: Print @qualid. + :name: Print This command displays on the screen information about the declared or defined object referred by :n:`@qualid`. @@ -34,8 +35,9 @@ Variants: .. cmdv:: Print Term @qualid. + :name: Print Term -This is a synonym to ``Print`` :n:`@qualid` when :n:`@qualid` +This is a synonym of :cmd:`Print` :n:`@qualid` when :n:`@qualid` denotes a global constant. .. cmdv:: About @qualid. @@ -50,7 +52,7 @@ argument scopes. It does not print the body of definitions or proofs. This locally renames the polymorphic universes of :n:`@qualid`. An underscore means the raw universe is printed. -This form can be used with ``Print Term`` and ``About``. +This form can be used with :cmd:`Print Term` and :cmd:`About`. .. cmd:: Print All. |