Add some refs in the Omega chapter.

1 files changed, 13 insertions, 13 deletions

diff --git a/doc/sphinx/addendum/omega.rst b/doc/sphinx/addendum/omega.rst
index e03431320..1e9d2aa1e 100644
--- a/doc/sphinx/addendum/omega.rst
+++ b/doc/sphinx/addendum/omega.rst
@@ -12,14 +12,14 @@ This tactic does not need any parameter:
 
 .. tacn:: omega
 
-``omega`` solves a goal in Presburger arithmetic, i.e. a universally
+:tacn:`omega` solves a goal in Presburger arithmetic, i.e. a universally
 quantified formula made of equations and inequations. Equations may
 be specified either on the type ``nat`` of natural numbers or on
 the type ``Z`` of binary-encoded integer numbers. Formulas on
 ``nat`` are automatically injected into ``Z``.  The procedure
 may use any hypothesis of the current proof session to solve the goal.
 
-Multiplication is handled by ``omega`` but only goals where at
+Multiplication is handled by :tacn:`omega` but only goals where at
 least one of the two multiplicands of products is a constant are
 solvable. This is the restriction meant by "Presburger arithmetic".
 
@@ -29,7 +29,7 @@ In any case, the computation eventually stops.
 Arithmetical goals recognized by ``omega``
 ------------------------------------------
 
-``omega`` applied only to quantifier-free formulas built from the
+:tacn:`omega` applied only to quantifier-free formulas built from the
 connectors::
 
    /\  \/  ~  ->
@@ -38,11 +38,11 @@ on atomic formulas. Atomic formulas are built from the predicates::
 
    =  <  <=  >  >=
 
-on ``nat`` or ``Z``. In expressions of type ``nat``, ``omega`` recognizes::
+on ``nat`` or ``Z``. In expressions of type ``nat``, :tacn:`omega` recognizes::
 
    +  -  *  S  O  pred
 
-and in expressions of type ``Z``, ``omega`` recognizes numeral constants and::
+and in expressions of type ``Z``, :tacn:`omega` recognizes numeral constants and::
 
    +  -  *  Z.succ Z.pred
 
@@ -53,22 +53,22 @@ were arbitrary variables of type ``nat`` or ``Z``.
 Messages from ``omega``
 -----------------------
 
-When ``omega`` does not solve the goal, one of the following errors
+When :tacn:`omega` does not solve the goal, one of the following errors
 is generated:
 
 .. exn:: omega can't solve this system.
 
   This may happen if your goal is not quantifier-free (if it is
-  universally quantified, try ``intros`` first; if it contains
-  existentials quantifiers too, ``omega`` is not strong enough to solve your
+  universally quantified, try :tacn:`intros` first; if it contains
+  existentials quantifiers too, :tacn:`omega` is not strong enough to solve your
   goal). This may happen also if your goal contains arithmetical
-  operators unknown from ``omega``. Finally, your goal may be really
+  operators unknown from :tacn:`omega`. Finally, your goal may be really
   wrong!
 
 .. exn:: omega: Not a quantifier-free goal.
 
   If your goal is universally quantified, you should first apply
-  ``intro`` as many time as needed.
+  :tacn:`intro` as many times as needed.
 
 .. exn:: omega: Unrecognized predicate or connective: @ident.
 
@@ -116,11 +116,11 @@ Options
 .. opt:: Stable Omega
 
 This deprecated option (on by default) is for compatibility with Coq pre 8.5. It
-resets internal name counters to make executions of ``omega`` independent.
+resets internal name counters to make executions of :tacn:`omega` independent.
 
 .. opt:: Omega UseLocalDefs
 
-This option (on by default) allows ``omega`` to use the bodies of local
+This option (on by default) allows :tacn:`omega` to use the bodies of local
 variables.
 
 .. opt:: Omega System
@@ -149,7 +149,7 @@ Overview of the tactic
 Overview of the OMEGA decision procedure
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
-The OMEGA decision procedure involved in the ``omega`` tactic uses
+The OMEGA decision procedure involved in the :tacn:`omega` tactic uses
 a small subset of the decision procedure presented in :cite:`TheOmegaPaper`
 Here is an overview, look at the original paper for more information.