Fix some issues in refman

doc/sphinx/addendum/nsatz.rst

@@ -44,7 +44,7 @@ files that declare the axioms used to define the real numbers, you can
 
    `radicalmax`
      bound when searching for r such that
-     :math:`c (P−Q) r = \sum_{i=1..s} S_i (P i − Q i)`.
+     :math:`c (P−Q)^r = \sum_{i=1..s} S_i (P_i − Q_i)`.
      This argument must be of type `N` (binary natural numbers).
 
    `strategy`

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

@@ -555,7 +555,7 @@ Creating Hints
             Hint Extern 5 ({?X1 = ?X2} + {?X1 <> ?X2}) =>
               generalize  X1, X2; decide equality : eqdec.
             Goal forall a b:list (nat * nat), {a = b} + {a <> b}.
-            info_auto.
+            info_auto with eqdec.
 
    .. cmd:: Hint Cut [ @hints_regexp ] {? : {+ @ident } }
 

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

@@ -25,7 +25,7 @@ Solvers for logic and equality
 
    Moreover, if it has nothing else to do, :tacn:`tauto` performs introductions.
    Therefore, the use of :tacn:`intros` in the previous proof is unnecessary.
-   :tacn:`tauto` can for instance for:
+   :tacn:`tauto` can for instance solve:
 
    .. example::