From cfc54842c2a71b7cdb8c59e3ce9fe4a13cedb5ae Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 19 Aug 2020 14:41:19 -0400 Subject: [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 --- doc/changelog/08-tools/12862-more-mod-checking.rst | 4 ++++ 1 file changed, 4 insertions(+) create mode 100644 doc/changelog/08-tools/12862-more-mod-checking.rst (limited to 'doc') 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 `_, fixes `#12845 + `_, by Jason Gross). -- cgit v1.2.3