diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-05-14 13:43:41 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-05-14 13:43:41 +0200 |
| commit | 9e3989f949c1e3f20031d9af5a7bc89d97f5a951 (patch) | |
| tree | a3bc0f6a7f80840f84109460a3169726ffffe590 /doc/sphinx/addendum | |
| parent | 4094a8c2cac668db112fc84f5d1b287eacbf6700 (diff) | |
| parent | 805d78d12443d9df646362c024bfa83466c27fdd (diff) | |
Merge PR #7374: [sphinx] More fatal warnings.
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 |
3 files changed, 13 insertions, 4 deletions
diff --git a/doc/sphinx/addendum/generalized-rewriting.rst b/doc/sphinx/addendum/generalized-rewriting.rst index f5237e4fb..e10e16c10 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 5f8c06484..152f4f655 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 009efd0d2..80ce01620 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`` ------------------------------------------ |