coq/test-suite/output-coqchk, branch master The formal proof system [coqchk] Look inside inner modules as well 2020-08-19T19:09:42+00:00 Jason Gross 2020-08-19T18:41:19+00:00 cfc54842c2a71b7cdb8c59e3ce9fe4a13cedb5ae 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 
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
[coqchk] Add test 2020-05-22T10:15:22+00:00 Pierre Roux 2020-04-11T17:35:20+00:00 4bab69688d91648ec1725f6294b7430622e6accf