Review #1

doc/sphinx/addendum/micromega.rst

@@ -152,19 +152,24 @@ and checked to be :math:`-1`.
    tactic *e.g.*, :math:`x = 10 * x / 10` is solved by :tacn:`lra`.
 
 .. tacn:: lra_Q @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: lra_R @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: sos_Q @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: sos_R @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: sos_Z @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 `lia`: a tactic for linear integer arithmetic
 ---------------------------------------------
@@ -231,10 +236,12 @@ with an equation :math:`e = i` for :math:`i \in [c_1,c_2]` and recursively searc
 a proof.
 
 .. tacn:: xlia @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: xnqa @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 `nra`: a proof procedure for non-linear arithmetic
 --------------------------------------------------
@@ -257,7 +264,8 @@ After this pre-processing, the linear prover of :tacn:`lra` searches for a
 proof by abstracting monomials by variables.
 
 .. tacn:: xnra @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 `nia`: a proof procedure for non-linear integer arithmetic
 ----------------------------------------------------------
@@ -269,7 +277,8 @@ proof by abstracting monomials by variables.
    solved using the linear integer prover :tacn:`lia`.
 
 .. tacn:: xnlia @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 `psatz`: a proof procedure for non-linear arithmetic
 ----------------------------------------------------
@@ -301,13 +310,16 @@ 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
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: psatz_R {? @nat_or_var } @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: psatz_Z {? @nat_or_var } @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 
 `zify`: pre-processing of arithmetic goals
@@ -360,19 +372,24 @@ 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
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: zify_iter_let @ltac_expr
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: zify_iter_specs
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: zify_op
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: zify_saturate
-   :undocumented:
+
+   For internal use only.
 
 
 .. [#csdp] Sources and binaries can be found at https://projects.coin-or.org/Csdp

doc/sphinx/addendum/ring.rst

@@ -193,10 +193,12 @@ Error messages:
   Same as above in the case of the :tacn:`ring` tactic.
 
 .. tacn:: ring_lookup @ltac_expr0 [ {* @one_term } ] {+ @one_term }
-   :undocumented:
+
+   For internal use only.
 
 .. tacn:: protect_fv @string {? in @ident }
-   :undocumented:
+
+   For internal use only.
 
 Adding a ring structure
 ----------------------------
@@ -620,7 +622,8 @@ Dealing with fields
      If specified, simplify in the hypothesis :n:`@ident` instead of the conclusion.
 
 .. tacn:: field_lookup @ltac_expr [ {* @one_term } ] {+ @one_term }
-   :undocumented:
+
+   For internal use only.
 
 Adding a new field structure
 ---------------------------------