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/proof-engine/ssreflect-proof-language.rst | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'doc/sphinx/proof-engine')

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