| Commit message (Collapse) | Author | Age |
|
|
|
|
|
|
|
|
|
|
| |
This is required for compatibility with
https://github.com/coq/coq/pull/8064, where prim token notations no longer
follow `Require`, but instead follow `Import`.
c.f. https://github.com/coq/coq/pull/8064#issuecomment-415493362
Almost all changes were made via
https://gist.github.com/JasonGross/5d4558edf8f5c2c548a3d96c17820169#file-fix-py
|
|
|
|
|
|
|
| |
With
```bash
bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh
```
|
|
* hopefully all proofs we need about xzladderstep
* Better automation in xzproofs
* Speed up xzproofs with heuristic clearing
* Remove useless hypotheses
* XZProofs cleanup
* fix "group by isomorphism" proofs, use in XZProofs
|