Miscellaneous small changes #2319
Conversation
|
Otherwise this looks good to me! |
|
I'll merge once the CI is done, unless @Alizter also wants to take a look. |
|
I would like to take a look tomorrow at the weekend if that's no problem. |
|
@Alizter Any idea what's up with the failure of coqchk? All I did is remove a comment when I force pushed, and I'm pretty sure all jobs succeeded when I first created this PR. |
|
I'm not certain. Since it's only dev that is failing it could be an upstream issue so that would have to be checked. I can take a look tomorrow if it persists. |
|
I re-ran the jobs, and there was no error this time, so it was just a temporary glitch. |
|
|
||
| (** This file contains all the tweaks and settings we make to Coq. *) | ||
|
|
||
| (** ** Warnings *) |
There was a problem hiding this comment.
I think I kept this as the natural place to include warnings. I don't feel strongly about keeping it but just FYI.
There was a problem hiding this comment.
Yeah, that's what I thought, but we may as well keep things simple until we need them.
3 participants
I've accumulated a bunch of small things. Each commit is independent and affects only one file, so they can be reviewed separately or together.