Require NsatzTactic: nsatz support for Z and Q

The purpose of `NsatzTactic` is to allow using `nsatz` without the
dependency on real axioms. So we declare the instances for `Z` and `Q`
in that file, so that users don't have to re-create them.

Fixes #12860

1 files changed, 7 insertions, 1 deletions

diff --git a/doc/sphinx/addendum/nsatz.rst b/doc/sphinx/addendum/nsatz.rst
index ed2e1ea58c..ed93145622 100644
--- a/doc/sphinx/addendum/nsatz.rst
+++ b/doc/sphinx/addendum/nsatz.rst
@@ -34,6 +34,12 @@ Nsatz: tactics for proving equalities in integral domains
 
    You can load the ``Nsatz`` module with the command ``Require Import Nsatz``.
 
+   Alternatively, if you prefer not to transitively depend on the
+   files declaring the axioms used to define the real numbers, you can
+   ``Require Import NsatzTactic`` instead; this will still allow
+   :tacn:`nsatz` to solve goals defined about :math:`\mathbb{Z}`,
+   :math:`\mathbb{Q}` and any user-registered rings.
+
 More about `nsatz`
 ---------------------
 
@@ -85,4 +91,4 @@ performed using :ref:`typeclasses`.
      then `lvar` is replaced by all the variables which are not in
      `parameters`.
 
-See the file `Nsatz.v` for many examples, especially in geometry.
+See the test-suite file `Nsatz.v <https://github.com/coq/coq/blob/master/test-suite/success/Nsatz.v>`_ for many examples, especially in geometry.