diff options
| author |  Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-04-29 00:38:54 +0200 |
|---|---|---|
| committer | Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr> | 2018-05-09 10:35:10 +0200 |
| commit | 88c702dfac4adb8bf590a2bdf30e76c7c6cb892f (patch) | |
| tree | a619bc1c3dd2c11fa6ce409cc6ba8fbb0759a648 /doc/sphinx/addendum | |
| parent | 52e58d368bb0646cc05684995d6e00da370736e6 (diff) | |
[sphinx] Fix new warnings related to tacn, cmd, opt...
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`` ------------------------------------------ |