From 1ccb800d20f91f1566d59b549a8422f2230c25d5 Mon Sep 17 00:00:00 2001 From: Théo Zimmermann Date: Tue, 24 Apr 2018 11:59:49 +0200 Subject: [sphinx] Use option direct reference. --- doc/sphinx/addendum/universe-polymorphism.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index c791fc906b..b8587d382d 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 -- cgit v1.2.3