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 +++---
 doc/sphinx/proof-engine/ssreflect-proof-language.rst | 13 ++++++++-----
 2 files changed, 11 insertions(+), 8 deletions(-)

(limited to 'doc/sphinx')

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
diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
index f8435fcffe..9ee61a801a 100644
--- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst
+++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst
@@ -2232,6 +2232,7 @@ tactics to *permute* the subgoals generated by a tactic.
       circular order of subgoals remains unchanged.
 
    .. tacn:: first @num last
+      :name: first (ssreflect)
 
       If :token:`num`\'s value is :math:`k`,
       this tactic rotates the :math:`n` subgoals :math:`G_1` , …, :math:`G_n`
@@ -5653,22 +5654,23 @@ respectively.
 
 .. tacn:: apply
           exact
+   :name: apply (ssreflect); exact (ssreflect)
 
    application (see :ref:`the_defective_tactics_ssr`)
 
-.. tacn:: abstract
+.. tacv:: abstract
 
    see :ref:`abstract_ssr` and :ref:`generating_let_ssr`
 
-.. tacn:: elim
+.. tacv:: elim
 
    induction (see :ref:`the_defective_tactics_ssr`)
 
-.. tacn:: case
+.. tacv:: case
 
    case analysis (see :ref:`the_defective_tactics_ssr`)
 
-.. tacn:: rewrite {+ @r_step }
+.. tacv:: rewrite {+ @r_step }
 
    rewrite (see :ref:`rewriting_ssr`)
 
@@ -5702,7 +5704,7 @@ respectively.
 
    backchaining (see :ref:`structure_ssr`)
 
-.. tacn:: pose @ident := @term
+.. tacv:: pose @ident := @term
 
    local definition (see :ref:`definitions_ssr`)
 
@@ -5719,6 +5721,7 @@ respectively.
    local cofix definition
 
 .. tacn:: set @ident {? : @term } := {? @occ_switch } {| @term | ( @c_pattern) }
+   :name: set (ssreflect)
 
    abbreviation (see :ref:`abbreviations_ssr`)
 
-- 
cgit v1.2.3