diff options
| -rw-r--r-- | doc/sphinx/addendum/ring.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/refman-preamble.rst | 1 |
2 files changed, 1 insertions, 2 deletions
diff --git a/doc/sphinx/addendum/ring.rst b/doc/sphinx/addendum/ring.rst index 027db9f47a..abfffa0035 100644 --- a/doc/sphinx/addendum/ring.rst +++ b/doc/sphinx/addendum/ring.rst @@ -382,7 +382,7 @@ The syntax for adding a new ring is that, given a term, “abstracts” it into an object of type |N| whose interpretation via ``Cp_phi`` (the evaluation function of power coefficient) is the original term, or returns ``InitialRing.NotConstant`` - if not a constant coefficient (i.e. |L_tac| is the inverse function of + if not a constant coefficient (i.e. |Ltac| is the inverse function of ``Cp_phi``). See files ``plugins/ring/ZArithRing.v`` and ``plugins/ring/RealField.v`` for examples. By default the tactic does not recognize power expressions as ring expressions. diff --git a/doc/sphinx/refman-preamble.rst b/doc/sphinx/refman-preamble.rst index 05e665a43b..e67405a8dc 100644 --- a/doc/sphinx/refman-preamble.rst +++ b/doc/sphinx/refman-preamble.rst @@ -20,7 +20,6 @@ .. |eq_beta_delta_iota_zeta| replace:: `=`\ :math:`_{\beta\delta\iota\zeta}` .. |Gallina| replace:: :smallcaps:`Gallina` .. |Latex| replace:: :smallcaps:`LaTeX` -.. |L_tac| replace:: `L`:sub:`tac` .. |Ltac| replace:: `L`:sub:`tac` .. |ML| replace:: :smallcaps:`ML` .. |OCaml| replace:: :smallcaps:`OCaml` |