Review #2

Author: jfehrle

doc/sphinx/addendum/micromega.rst

@@ -152,20 +152,16 @@ and checked to be :math:`-1`.
    tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`.
 
 .. tacn:: lra_Q @ltac_expr
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: lra_R @ltac_expr
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: sos_Q @ltac_expr
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: sos_R @ltac_expr
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: sos_Z @ltac_expr
 
@@ -236,8 +232,7 @@ with an equation :math:`e = i` for :math:`i \in [c_1,c_2]` and recursively searc
 a proof.
 
 .. tacn:: xlia @ltac_expr
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: xnqa @ltac_expr
 
@@ -310,12 +305,10 @@ belongs to :math:`\mathit{Cone}({−x^2,x -1})`. Moreover, by running :tacn:`rin
 obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
 
 .. tacn:: psatz_Q {? @nat_or_var } @ltac_expr
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: psatz_R {? @nat_or_var } @ltac_expr
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: psatz_Z {? @nat_or_var } @ltac_expr
 
@@ -372,20 +365,16 @@ obtain :math:`-1`. By Theorem :ref:`Psatz <psatz_thm>`, the goal is valid.
    :g:`Z`, :g:`nat`, :g:`positive` and :g:`N`.
 
 .. tacn:: zify_elim_let
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: zify_iter_let @ltac_expr
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: zify_iter_specs
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: zify_op
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: zify_saturate
 

doc/sphinx/addendum/ring.rst

@@ -193,8 +193,7 @@ Error messages:
   Same as above in the case of the :tacn:`ring` tactic.
 
 .. tacn:: ring_lookup @ltac_expr0 [ {* @one_term } ] {+ @one_term }
-
-   For internal use only.
+   :undocumented:
 
 .. tacn:: protect_fv @string {? in @ident }
 

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

@@ -140,7 +140,8 @@ Programmable proof search
       `breadth-first search <https://en.wikipedia.org/wiki/Breadth-first_search>`_.
 
    .. tacn:: dfs eauto {? @nat_or_var } {? @auto_using } {? @hintbases }
-      :undocumented:
+
+      An alias for :tacn:`eauto`.
 
 .. tacn:: autounfold {? @hintbases } {? @simple_occurrences }