diff options
| author | Jim Fehrle | 2020-05-06 16:12:47 -0700 |
|---|---|---|
| committer | Jim Fehrle | 2020-06-08 16:50:53 -0700 |
| commit | 6a76e4394876cb08b02d8e7ea185049147f9cd2b (patch) | |
| tree | 630347daab79b5e49263150fba6c3e5baee09c8a /doc/sphinx/addendum | |
| parent | 11baeeeba16faa3d402489ee3423103ef2511044 (diff) | |
Make automatic name generation for directives more consistent:
- by default, generate names for all directives using the prefix "[a-zA-Z0-9_ ]+" except
- don't generate a name for cmdv and tacv
- generate more flexibily for exn, warn and attr
Diffstat (limited to 'doc/sphinx/addendum')
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 2a321b5cbf..f037fed394 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -102,7 +102,7 @@ forget this paragraph and use the tactic according to your intuition. Concrete usage in Coq -------------------------- -.. tacn:: ring +.. tacv:: ring This tactic solves equations upon polynomial expressions of a ring (or semiring) structure. It proceeds by normalizing both sides @@ -110,7 +110,7 @@ Concrete usage in Coq distributivity, constant propagation, rewriting of monomials) and comparing syntactically the results. -.. tacn:: ring_simplify +.. tacv:: ring_simplify This tactic applies the normalization procedure described above to the given terms. The tactic then replaces all occurrences of the terms @@ -511,7 +511,7 @@ application of the main correctness theorem to well-chosen arguments. Dealing with fields ------------------------ -.. tacn:: field +.. tacv:: field This tactic is an extension of the :tacn:`ring` tactic that deals with rational expressions. Given a rational expression :math:`F = 0`. It first reduces the |