From 6a76e4394876cb08b02d8e7ea185049147f9cd2b Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Wed, 6 May 2020 16:12:47 -0700
Subject: 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

---
 doc/sphinx/addendum/ring.rst | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'doc/sphinx/addendum')

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
-- 
cgit v1.2.3