diff options
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/generalized-rewriting.rst | 3 | ||||
| -rw-r--r-- | doc/sphinx/addendum/implicit-coercions.rst | 9 | ||||
| -rw-r--r-- | doc/sphinx/addendum/omega.rst | 5 | ||||
| -rw-r--r-- | doc/sphinx/addendum/universe-polymorphism.rst | 2 |
4 files changed, 14 insertions, 5 deletions
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index f5237e4fbf..e10e16c107 100644 --- a/doc/sphinx/addendum/generalized-rewriting.rst +++ b/doc/sphinx/addendum/generalized-rewriting.rst @@ -599,6 +599,7 @@ Notice that the syntax is not completely backward compatible since the identifier was not required. .. cmd:: Add Morphism f : @ident + :name: Add Morphism The latter command also is restricted to the declaration of morphisms without parameters. It is not fully backward compatible since the @@ -616,7 +617,7 @@ the same signature. Finally, the :tacn:`replace` and :tacn:`rewrite` tactics can used to replace terms in contexts that were refused by the old implementation. As discussed in the next section, the semantics of the new :tacn:`setoid_rewrite` tactic differs slightly from the old one and -tacn:`rewrite`. +:tacn:`rewrite`. Extensions diff --git a/doc/sphinx/addendum/implicit-coercions.rst b/doc/sphinx/addendum/implicit-coercions.rst index 5f8c064840..152f4f6552 100644 --- a/doc/sphinx/addendum/implicit-coercions.rst +++ b/doc/sphinx/addendum/implicit-coercions.rst @@ -263,9 +263,12 @@ Activating the Printing of Coercions .. cmd:: Add Printing Coercion @qualid - This command forces coercion denoted by :n:`@qualid` to be printed. To skip - the printing of coercion :n:`@qualid`, use :cmd:`Remove Printing Coercion`. By - default, a coercion is never printed. + This command forces coercion denoted by :n:`@qualid` to be printed. + By default, a coercion is never printed. + +.. cmd:: Remove Printing Coercion @qualid + + Use this command, to skip the printing of coercion :n:`@qualid`. .. _coercions-classes-as-records: diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst index 009efd0d25..80ce016200 100644 --- a/doc/sphinx/addendum/omega.rst +++ b/doc/sphinx/addendum/omega.rst @@ -26,6 +26,11 @@ solvable. This is the restriction meant by "Presburger arithmetic". If the tactic cannot solve the goal, it fails with an error message. In any case, the computation eventually stops. +.. tacv:: romega + :name: romega + + To be documented. + Arithmetical goals recognized by ``omega`` ------------------------------------------ diff --git a/doc/sphinx/addendum/universe-polymorphism.rst b/doc/sphinx/addendum/universe-polymorphism.rst index e80cfb6bb5..6e7ccba63c 100644 --- a/doc/sphinx/addendum/universe-polymorphism.rst +++ b/doc/sphinx/addendum/universe-polymorphism.rst @@ -412,7 +412,7 @@ end of a definition or proof, we check that the only remaining universes are the ones declared. In the term and in general in proof mode, introduced universe names can be referred to in terms. Note that local universe names shadow global universe names. During a proof, one -can use :ref:`Show Universes <ShowUniverses>` to display the current context of universes. +can use :cmd:`Show Universes` to display the current context of universes. Definitions can also be instantiated explicitly, giving their full instance: |