Require NsatzTactic: nsatz support for Z and Q #12861
Conversation
|
For your complete information, the job test-suite:4.11+trunk+dune in allow failure mode has failed for commit f67d6e6: Require NsatzTactic: nsatz support for Z and Q |
There was a problem hiding this comment.
Looks good but maybe there should be a footnote in the doc https://coq.inria.fr/refman/addendum/nsatz.html that tells what is going on.
|
Documentation updated; is this approximately what you were thinking of? |
|
For your complete information, the job test-suite:4.11+trunk+dune in allow failure mode has failed for commit 021f02d: Update nsatz documentation, as requested |
doc/changelog/10-standard-library/12861-nsatz-tactic-instances.rst
Outdated
Show resolved
Hide resolved
|
For your complete information, the job test-suite:4.11+trunk+dune in allow failure mode has failed for commit 9c12116: Apply suggestions from code review |
|
@JasonGross this should probably be squashed |
|
Squashing the documentation commits looks like a good idea indeed, but it's not mandatory either. I'll merge soon anyways. |
|
Please squash before the merge. The individual commits are not interesting, more noise in the git history. |
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 coq#12860
JasonGross
force-pushed
the
nsatz-tactic-instances
branch
from
dea629c
to
4ad36b5
Compare
|
I've squashed all the commits. |
ppedrot
added
kind: fix
The purpose of
NsatzTacticis to allow usingnsatzwithout thedependency on real axioms. So we declare the instances for
ZandQin that file, so that users don't have to re-create them.
Fixes #12860
Kind: bug fix / enhancement
Fixes / closes #12860