aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-04-24 11:59:49 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-05-05 11:54:02 +0200
commit1ccb800d20f91f1566d59b549a8422f2230c25d5 (patch)
tree4eaf99e6a3b9eb7197e6e9b08b4675c8720ca60e /doc
parent75715450906ffbf65a4f7a9f92031dd00ac96ead (diff)
[sphinx] Use option direct reference.
Diffstat (limited to 'doc')
-rw-r--r--doc/sphinx/addendum/universe-polymorphism.rst8
1 files changed, 4 insertions, 4 deletions
diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst
index c791fc906..b8587d382 100644
--- a/doc/sphinx/addendum/universe-polymorphism.rst
+++ b/doc/sphinx/addendum/universe-polymorphism.rst
@@ -79,7 +79,7 @@ levels.
When printing :g:`pidentity`, we can see the universes it binds in
the annotation :g:`@{Top.2}`. Additionally, when
-:g:`Set Printing Universes` is on we print the "universe context" of
+:opt:`Printing Universes` is on we print the "universe context" of
:g:`pidentity` consisting of the bound universes and the
constraints they must verify (for :g:`pidentity` there are no constraints).
@@ -169,7 +169,7 @@ declared cumulative using the :g:`Cumulative` prefix.
Declares the inductive as cumulative
-Alternatively, there is an option :g:`Set Polymorphic Inductive
+Alternatively, there is an option :opt:`Polymorphic Inductive
Cumulativity` which when set, makes all subsequent *polymorphic*
inductive definitions cumulative. When set, inductive types and the
like can be enforced to be non-cumulative using the :g:`NonCumulative`
@@ -229,7 +229,7 @@ Cumulative inductive types, coninductive types, variants and records
only make sense when they are universe polymorphic. Therefore, an
error is issued whenever the user uses the :g:`Cumulative` or
:g:`NonCumulative` prefix in a monomorphic context.
-Notice that this is not the case for the option :g:`Set Polymorphic Inductive Cumulativity`.
+Notice that this is not the case for the option :opt:`Polymorphic Inductive Cumulativity`.
That is, this option, when set, makes all subsequent *polymorphic*
inductive declarations cumulative (unless, of course the :g:`NonCumulative` prefix is used)
but has no effect on *monomorphic* inductive declarations.
@@ -438,7 +438,7 @@ underscore or by omitting the annotation to a polymorphic definition.
.. opt:: Strict Universe Declaration.
- The command ``Unset Strict Universe Declaration`` allows one to freely use
+ Turning this option off allows one to freely use
identifiers for universes without declaring them first, with the
semantics that the first use declares it. In this mode, the universe
names are not associated with the definition or proof once it has been