| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-12-03 | Changes for Coq 8.13 | Matthieu Sozeau | |
| 2020-08-19 | [coqchk] Look inside inner modules as well | Jason Gross | |
| 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 | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |