[doc] Small fixes

3 files changed, 26 insertions, 23 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index f887a5fee..0e9c23b9b 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -150,9 +150,10 @@ are a way to take into account the discreteness of :math:`\mathbb{Z}` by roundin
 
 .. _ceil_thm:
 
-**Theorem**. Let :math:`p` be an integer and :math:`c` a rational constant. Then
+.. thm:: Bound on the ceiling function
 
- :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`
+   Let :math:`p` be an integer and :math:`c` a rational constant. Then
+   :math:`p \ge c \rightarrow p \ge \lceil{c}\rceil`.
 
 For instance, from 2 x = 1 we can deduce
 
diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst
index 0318bddde..3835524f0 100644
--- a/doc/sphinx/proof-engine/tactics.rst
+++ b/doc/sphinx/proof-engine/tactics.rst
@@ -653,7 +653,7 @@ be applied or the goal is not head-reducible.
    This repeats ``intro`` until it meets the head-constant. It never
    reduces head-constants and it never fails.
 
-.. tac:: intro @ident
+.. tacn:: intro @ident
 
    This applies ``intro`` but forces :n:`@ident` to be the name of the
    introduced hypothesis.
@@ -904,15 +904,15 @@ quantification or an implication.
 .. tacn:: revert {+ @ident}
    :name: revert
 
-This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses
-(possibly defined) to the goal, if this respects dependencies. This tactic is
-the inverse of :tacn:`intro`.
+   This applies to any goal with variables :n:`{+ @ident}`. It moves the hypotheses
+   (possibly defined) to the goal, if this respects dependencies. This tactic is
+   the inverse of :tacn:`intro`.
 
 .. exn:: No such hypothesis.
 
 .. exn:: @ident is used in the hypothesis @ident.
 
-.. tac:: revert dependent @ident
+.. tacn:: revert dependent @ident
 
    This moves to the goal the hypothesis :n:`@ident` and all the hypotheses that
    depend on it.
@@ -1122,7 +1122,7 @@ Controlling the proof flow
    This behaves as :n:`assert (@ident : form)` but :n:`@ident` is generated by
    Coq.
 
-.. tacv:: assert form by tactic
+.. tacv:: assert @form by @tactic
 
    This tactic behaves like :n:`assert` but applies tactic to solve the subgoals
    generated by assert.
@@ -1130,7 +1130,7 @@ Controlling the proof flow
    .. exn:: Proof is not complete.
       :name: Proof is not complete. (assert)
 
-.. tacv:: assert form as intro_pattern
+.. tacv:: assert @form as @intro_pattern
 
    If :n:`intro_pattern` is a naming introduction pattern (see :tacn:`intro`),
    the hypothesis is named after this introduction pattern (in particular, if
@@ -1139,7 +1139,7 @@ Controlling the proof flow
    introduction pattern, the tactic behaves like :n:`assert form` followed by
    the action done by this introduction pattern.
 
-.. tacv:: assert form as intro_pattern by tactic
+.. tacv:: assert @form as @intro_pattern by @tactic
 
    This combines the two previous variants of :n:`assert`.
 
@@ -1192,9 +1192,9 @@ Controlling the proof flow
    This behaves like :n:`enough form` using :n:`intro_pattern` to name or
    destruct the new hypothesis.
 
-.. tacv:: enough (@ident : form) by tactic
-.. tacv:: enough form by tactic
-.. tacv:: enough form as intro_pattern by tactic
+.. tacv:: enough (@ident : @form) by @tactic
+.. tacv:: enough @form by @tactic
+.. tacv:: enough @form as @intro_pattern by @tactic
 
    This behaves as above but with :n:`tactic` expected to solve the initial goal
    after the extra assumption :n:`form` is added and possibly destructed. If the
@@ -3240,7 +3240,9 @@ the processing of the rewriting rules.
 The rewriting rule bases are built with the ``Hint Rewrite vernacular``
 command.
 
-.. warn:: This tactic may loop if you build non terminating rewriting systems.
+.. warning::
+
+   This tactic may loop if you build non terminating rewriting systems.
 
 .. tacv:: autorewrite with {+ @ident} using @tactic
 
@@ -3444,7 +3446,7 @@ The general command to add a hint to some databases :n:`{+ @ident}` is
 
       Declares each :n:`@ident` as a transparent or opaque constant.
 
-   .. cmdv:: Hint Extern @num {? @pattern} => tactic
+   .. cmdv:: Hint Extern @num {? @pattern} => @tactic
       :name: Hint Extern
 
       This hint type is to extend :tacn:`auto` with tactics other than :tacn:`apply` and
diff --git a/doc/sphinx/user-extensions/proof-schemes.rst b/doc/sphinx/user-extensions/proof-schemes.rst
index 682553c31..838926d65 100644
--- a/doc/sphinx/user-extensions/proof-schemes.rst
+++ b/doc/sphinx/user-extensions/proof-schemes.rst
@@ -106,15 +106,15 @@ Automatic declaration of schemes
 
 .. opt:: Elimination Schemes
 
-It is possible to deactivate the automatic declaration of the
-induction principles when defining a new inductive type with the
-``Unset Elimination Schemes`` command. It may be reactivated at any time with
-``Set Elimination Schemes``.
+   It is possible to deactivate the automatic declaration of the
+   induction principles when defining a new inductive type with the
+   ``Unset Elimination Schemes`` command. It may be reactivated at any time with
+   ``Set Elimination Schemes``.
 
 .. opt:: Nonrecursive Elimination Schemes
 
-This option controls whether types declared with the keywords :cmd:`Variant` and
-:cmd:`Record` get an automatic declaration of the induction principles.
+   This option controls whether types declared with the keywords :cmd:`Variant` and
+   :cmd:`Record` get an automatic declaration of the induction principles.
 
 .. opt:: Case Analysis Schemes
 
@@ -125,8 +125,8 @@ This option controls whether types declared with the keywords :cmd:`Variant` and
 
 .. opt:: Decidable Equality Schemes
 
-These flags control the automatic declaration of those Boolean equalities (see
-the second variant of ``Scheme``).
+   These flags control the automatic declaration of those Boolean equalities (see
+   the second variant of ``Scheme``).
 
 .. warning::