diff options
Diffstat (limited to 'doc/sphinx/proof-engine')
| -rw-r--r-- | doc/sphinx/proof-engine/ssreflect-proof-language.rst | 13 |
1 files changed, 8 insertions, 5 deletions
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`) |