Document various undocumented tactics

doc/sphinx/addendum/generalized-rewriting.rst

@@ -535,10 +535,11 @@ pass additional arguments such as ``using relation``.
 .. tacn:: setoid_reflexivity
           setoid_symmetry {? in @ident }
           setoid_transitivity @one_term
+          setoid_etransitivity
           setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } {? at @rewrite_occs } {? in @ident }
           setoid_rewrite {? {| -> | <- } } @one_term {? with @bindings } in @ident at @rewrite_occs
           setoid_replace @one_term with @one_term {? using relation @one_term } {? in @ident } {? at {+ @int_or_var } } {? by @ltac_expr3 }
-   :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_rewrite; _; setoid_replace
+   :name: setoid_reflexivity; setoid_symmetry; setoid_transitivity; setoid_etransitivity; setoid_rewrite; _; setoid_replace
 
    .. todo: move rewrite_occs to rewrite chapter when that chapter is revised
 

doc/sphinx/addendum/implicit-coercions.rst

@@ -127,7 +127,6 @@ Declaring Coercions
 
 .. cmd:: Coercion @reference : @class >-> @class
          Coercion @ident {? @univ_decl } @def_body
-
    :name: Coercion; _
 
   The first form declares the construction denoted by :token:`reference` as a coercion between

doc/sphinx/addendum/micromega.rst

@@ -151,6 +151,21 @@ and checked to be :math:`-1`.
    The deductive power of :tacn:`lra` overlaps with the one of :tacn:`field`
    tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`.
 
+.. tacn:: lra_Q @ltac_expr
+   :undocumented:
+
+.. tacn:: lra_R @ltac_expr
+   :undocumented:
+
+.. tacn:: sos_Q @ltac_expr
+   :undocumented:
+
+.. tacn:: sos_R @ltac_expr
+   :undocumented:
+
+.. tacn:: sos_Z @ltac_expr
+   :undocumented:
+
 `lia`: a tactic for linear integer arithmetic
 ---------------------------------------------
 
@@ -215,6 +230,12 @@ Our current oracle tries to find an expression :math:`e` with a small range
 with an equation :math:`e = i` for :math:`i \in [c_1,c_2]` and recursively search for
 a proof.
 
+.. tacn:: xlia @ltac_expr
+   :undocumented:
+
+.. tacn:: xnqa @ltac_expr
+   :undocumented:
+
 `nra`: a proof procedure for non-linear arithmetic
 --------------------------------------------------
 
@@ -235,6 +256,9 @@ a proof.
 After this pre-processing, the linear prover of :tacn:`lra` searches for a
 proof by abstracting monomials by variables.
 
+.. tacn:: xnra @ltac_expr
+   :undocumented:
+
 `nia`: a proof procedure for non-linear integer arithmetic
 ----------------------------------------------------------
 
@@ -244,6 +268,9 @@ proof by abstracting monomials by variables.
    It performs a pre-processing similar to :tacn:`nra`. The obtained goal is
    solved using the linear integer prover :tacn:`lia`.
 
+.. tacn:: xnlia @ltac_expr
+   :undocumented:
+
 `psatz`: a proof procedure for non-linear arithmetic
 ----------------------------------------------------
 
@@ -273,6 +300,16 @@ cone expression :math:`2 \times (x-1) + (\mathbf{x-1}) \times (\mathbf{x−1}) +
 belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`ring` we
 obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 
+.. tacn:: psatz_Q {? @nat_or_var } @ltac_expr
+   :undocumented:
+
+.. tacn:: psatz_R {? @nat_or_var } @ltac_expr
+   :undocumented:
+
+.. tacn:: psatz_Z {? @nat_or_var } @ltac_expr
+   :undocumented:
+
+
 `zify`: pre-processing of arithmetic goals
 ------------------------------------------
 
@@ -322,6 +359,21 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    prints the list of types that supported by :tacn:`zify` i.e.,
    :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
 
+.. tacn:: zify_elim_let
+   :undocumented:
+
+.. tacn:: zify_iter_let @ltac_expr
+   :undocumented:
+
+.. tacn:: zify_iter_specs
+   :undocumented:
+
+.. tacn:: zify_op
+   :undocumented:
+
+.. tacn:: zify_saturate
+   :undocumented:
+
 
 .. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp
 .. [#fnpsatz] Variants deal with equalities and strict inequalities.

doc/sphinx/addendum/nsatz.rst

@@ -94,3 +94,6 @@ Buchberger algorithm.
 
 This computation is done after a step of *reification*, which is
 performed using :ref:`typeclasses`.
+
+.. tacn:: nsatz_compute @one_term
+   :undocumented:

doc/sphinx/addendum/ring.rst

@@ -192,6 +192,11 @@ Error messages:
 
   Same as above in the case of the :tacn:`ring` tactic.
 
+.. tacn:: ring_lookup @ltac_expr0 [ {* @one_term } ] {+ @one_term }
+   :undocumented:
+
+.. tacn:: protect_fv @string {? in @ident }
+   :undocumented:
 
 Adding a ring structure
 ----------------------------
@@ -614,6 +619,8 @@ Dealing with fields
    :n:`in @ident`
      If specified, simplify in the hypothesis :n:`@ident` instead of the conclusion.
 
+.. tacn:: field_lookup @ltac_expr [ {* @one_term } ] {+ @one_term }
+   :undocumented:
 
 Adding a new field structure
 ---------------------------------

doc/sphinx/proofs/automatic-tactics/auto.rst

@@ -139,6 +139,9 @@ Programmable proof search
       Like :tacn:`eauto`, but uses a
       `breadth-first search <https://en.wikipedia.org/wiki/Breadth-first_search>`_.
 
+   .. tacn:: dfs eauto {? @nat_or_var } {? @auto_using } {? @hintbases }
+      :undocumented:
+
 .. tacn:: autounfold {? @hintbases } {? @simple_occurrences }
 
    Unfolds constants that were declared through a :cmd:`Hint Unfold`
@@ -147,6 +150,9 @@ Programmable proof search
    :n:`@simple_occurrences`
      Performs the unfolding in the specified occurrences.
 
+.. tacn:: autounfold_one {? @hintbases } {? in @ident }
+   :undocumented:
+
 .. tacn:: autorewrite {? * } with {+ @ident } {? @occurrences } {? using @ltac_expr }
 
    `*`
@@ -447,7 +453,7 @@ Creating Hints
    .. cmd:: Hint Unfold {+ @qualid } {? : {+ @ident } }
 
       For each :n:`@qualid`, adds the tactic :tacn:`unfold` :n:`@qualid` to the
-      hint list that will only be used when the head constant of the goal is :token:`qualid`.
+      hint list that will only be used when the :term:`head constant` of the goal is :token:`qualid`.
       Its cost is 4.
 
    .. cmd:: Hint {| Transparent | Opaque } {+ @qualid } {? : {+ @ident } }

doc/sphinx/proofs/automatic-tactics/logic.rst

@@ -87,6 +87,9 @@ Solvers for logic and equality
       This :term:`flag` controls whether :tacn:`intuition` unfolds inner negations which do not need
       to be unfolded. It is on by default.
 
+.. tacn:: gintuition {? @ltac_expr }
+   :undocumented:
+
 .. tacn:: rtauto
 
    Solves propositional tautologies similarly to
@@ -198,7 +201,7 @@ Solvers for logic and equality
       additional arguments can be given to congruence by filling in the holes in the
       terms given in the error message, using the `with` clause.
 
-   :opt:`Debug` ``"congruence"`` makes :tacn:`congruence` print debug information.
+   Setting :opt:`Debug` ``"congruence"`` makes :tacn:`congruence` print debug information.
 
 .. tacn:: btauto
 

doc/sphinx/proofs/writing-proofs/reasoning-inductives.rst

@@ -650,6 +650,9 @@ This section describes some special purpose tactics to work with
       implicitly added to this table when defined.
       Use the :cmd:`Add` and :cmd:`Remove` commands to update this set manually.
 
+.. tacn:: simple injection {? @induction_arg }
+   :undocumented:
+
 .. tacn:: simplify_eq {? @induction_arg }
 
    Examines a hypothesis that has the form :n:`@term__1 = @term__2`.  If the terms are

doc/sphinx/using/libraries/funind.rst

@@ -219,6 +219,9 @@ Tactics
    .. exn:: Not the right number of induction arguments.
       :undocumented:
 
+.. tacn:: soft functional induction {+ @one_term } {? using @one_term {? with @bindings } } {? as @simple_intropattern }
+   :undocumented:
+
 .. tacn:: functional inversion {| @ident | @natural } {? @qualid }
 
    Performs inversion on hypothesis