aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativecode.mli
diff options
context:
space:
mode:
authorJason Gross2020-08-19 14:41:19 -0400
committerJason Gross2020-08-19 15:09:42 -0400
commitcfc54842c2a71b7cdb8c59e3ce9fe4a13cedb5ae (patch)
tree89496379adc0ab698f89dcd6d5d790abfcc8c488 /kernel/nativecode.mli
parentb409b9837ce438042bb259d16a1b5156a2e0acb9 (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 'kernel/nativecode.mli')
0 files changed, 0 insertions, 0 deletions