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 /kernel/nativelambda.ml | |
| 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 'kernel/nativelambda.ml')
0 files changed, 0 insertions, 0 deletions