[sphinx] Fix some references.

4 files changed, 12 insertions, 13 deletions

diff --git a/doc/sphinx/addendum/micromega.rst b/doc/sphinx/addendum/micromega.rst
index 4f8cc34d4..f887a5fee 100644
--- a/doc/sphinx/addendum/micromega.rst
+++ b/doc/sphinx/addendum/micromega.rst
@@ -113,7 +113,7 @@ tactic *e.g.*, :math:`x = 10 * x / 10` is solved by `lra`.
 .. tacn:: lia
    :name: lia
 
-This tactic offers an alternative to the :tacn:`omega` and :tac:`romega`
+This tactic offers an alternative to the :tacn:`omega` and :tacn:`romega`
 tactics. Roughly speaking, the deductive power of lia is the combined deductive
 power of :tacn:`ring_simplify` and :tacn:`omega`. However, it solves linear
 goals that :tacn:`omega` and :tacn:`romega` do not solve, such as the following
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index a9c4dd758..c87bdd190 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -678,7 +678,7 @@ These are synonyms of the Definition forms.
 
 .. exn:: The term @term has type @type while it is expected to have type @type
 
-See also :cmd:`Opaque`, :cmd:`Transparent`, :tac:`unfold`.
+See also :cmd:`Opaque`, :cmd:`Transparent`, :tacn:`unfold`.
 
 .. cmd:: Let @ident := @term.
 
diff --git a/doc/sphinx/proof-engine/ltac.rst b/doc/sphinx/proof-engine/ltac.rst
index 7ab11889f..b70c79f68 100644
--- a/doc/sphinx/proof-engine/ltac.rst
+++ b/doc/sphinx/proof-engine/ltac.rst
@@ -1223,7 +1223,7 @@ performance bug.
 
    .. warning::
 
-      Backtracking across a Reset Ltac Profile will not restore the information.
+      Backtracking across a :cmd:`Reset Ltac Profile` will not restore the information.
 
 .. coqtop:: reset in
 
@@ -1286,8 +1286,8 @@ performance bug.
    benchmarking purposes.
 
 You can also pass the ``-profile-ltac`` command line option to ``coqc``, which
-performs a ``Set Ltac Profiling`` at the beginning of each document, and a
-``Show Ltac Profile`` at the end.
+turns the :opt:`Ltac Profiling` option on at the beginning of each document,
+and performs a :cmd:`Show Ltac Profile` at the end.
 
 .. warning::
 
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst
index f62e95669..64e28cea4 100644
--- a/doc/sphinx/proof-engine/proof-handling.rst
+++ b/doc/sphinx/proof-engine/proof-handling.rst
@@ -542,13 +542,13 @@ debugging universe inconsistencies.
 
 .. cmd:: Guarded.
 
-Some tactics (e.g. :tacn:`refine` :ref:`applyingtheorems`) allow to build proofs using
+Some tactics (e.g. :tacn:`refine`) allow to build proofs using
 fixpoint or co-fixpoint constructions. Due to the incremental nature
 of interactive proof construction, the check of the termination (or
 guardedness) of the recursive calls in the fixpoint or cofixpoint
 constructions is postponed to the time of the completion of the proof.
 
-The command ``Guarded`` allows checking if the guard condition for
+The command :cmd:`Guarded` allows checking if the guard condition for
 fixpoint and cofixpoint is violated at some time of the construction
 of the proof without having to wait the completion of the proof.
 
@@ -570,13 +570,12 @@ available hypotheses.
 
 This option controls the way binders are handled
 in assertion commands such as ``Theorem ident [binders] : form``. When the
-option is set, which is the default, binders are automatically put in
+option is on, which is the default, binders are automatically put in
 the local context of the goal to prove.
 
-The option can be unset by issuing ``Unset Automatic Introduction``. When
-the option is unset, binders are discharged on the statement to be
-proved and a tactic such as intro (see Section :ref:`managingthelocalcontext`) has to be
-used to move the assumptions to the local context.
+When the option is off, binders are discharged on the statement to be
+proved and a tactic such as :tacn:`intro` (see Section :ref:`managingthelocalcontext`)
+has to be used to move the assumptions to the local context.
 
 
 Controlling memory usage
@@ -597,4 +596,4 @@ the ongoing proof.
 This command forces the |OCaml| runtime to perform a heap compaction.
 This is in general an expensive operation.
 See: `OCaml Gc <http://caml.inria.fr/pub/docs/manual-ocaml/libref/Gc.html#VALcompact>`_
-There is also an analogous tactic :tac:`optimize_heap`.
+There is also an analogous tactic :tacn:`optimize_heap`.