diff options
| author | Jason Gross | 2020-08-19 14:41:19 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-08-19 15:09:42 -0400 |
| commit | cfc54842c2a71b7cdb8c59e3ce9fe4a13cedb5ae (patch) | |
| tree | 89496379adc0ab698f89dcd6d5d790abfcc8c488 /doc | |
| parent | b409b9837ce438042bb259d16a1b5156a2e0acb9 (diff) | |
[coqchk] Look inside inner modules as well
Fixes #12845 (coqchk reports names from inner modules of opaque modules
as axioms)
I don't fully understand the code here, so I can't speak as to its
correctness, but it should be simple enough that reviewers can
understand what it's doing and whether or not it's correct.
This is useful for me in making progress towards
https://github.com/mit-plv/fiat-crypto/issues/736
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/changelog/08-tools/12862-more-mod-checking.rst | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/doc/changelog/08-tools/12862-more-mod-checking.rst b/doc/changelog/08-tools/12862-more-mod-checking.rst new file mode 100644 index 0000000000..bb1bf9e789 --- /dev/null +++ b/doc/changelog/08-tools/12862-more-mod-checking.rst @@ -0,0 +1,4 @@ +- **Fixed:** + ``coqchk`` no longer reports names from inner modules of opaque modules as + axioms (`#12862 <https://github.com/coq/coq/pull/12862>`_, fixes `#12845 + <https://github.com/coq/coq/issues/12845>`_, by Jason Gross). |