diff options
| author | Jason Gross | 2020-08-19 13:07:14 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-08-25 14:58:50 -0400 |
| commit | 4ad36b5e2369b37aa2483a1e04eb628d147d97d3 (patch) | |
| tree | 2076e0c62e8e571dc64d2775377f6dd24ffabea9 /doc | |
| parent | 51c0d56a5b0384e2f6bd980a1111547641c66b3e (diff) | |
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
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst | 7 | ||||
| -rw-r--r-- | doc/sphinx/addendum/nsatz.rst | 8 |
2 files changed, 14 insertions, 1 deletions
diff --git a/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst b/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst new file mode 100644 index 0000000000..41359098e3 --- /dev/null +++ b/doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst @@ -0,0 +1,7 @@ +- **Changed:** + ``Require Import Coq.nsatz.NsatzTactic`` now allows using :tacn:`nsatz` + with `Z` and `Q` without having to supply instances or using ``Require Import Coq.nsatz.Nsatz``, which + transitively requires unneeded files declaring axioms used in the reals + (`#12861 <https://github.com/coq/coq/pull/12861>`_, + fixes `#12860 <https://github.com/coq/coq/issues/12860>`_, + by Jason Gross). 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. |