Robbert Krebbers
Robbert Krebbers
With the `using` attribute one can make sure that a `Definition` is generalized over a section variable regardless of whether it is used. For example: ```coq Section foo. Context (a...
#### Version 8.7.1 #### Operating system Linux #### Description of the problem According to the manual, `Set Typeclasses Unique Instances` makes sure that "when a solution to the typeclass goal...
The name `diris` was still there for legacy purposes, it should be consistent with the name of the repo.
This information is not in the README. I think it would be good to include it there.
I tried to compile and run the development with Coq 8.17 and get some errors and warnings. The errors are about `Global` being missing, I will open a pull request...
### Is your feature request related to a problem? Currently there is the `Unset Elimination Schemes` command to disable the generation of induction schemes. It would be much nicer, and...
### Description of the problem https://github.com/coq/coq/pull/19049 introduced new warnings. These warnings should be disabled for "printing only" notations since parsing is irrelevant there. This issue shows up with the proofmode...
When inviting an external reviewer, HotCRP performs a check for conflicts of interest. This check happens after filling the form and pressing the "Request review" button. In practice, one often...
It would be very useful if HotCRP has an option that allows administrators to disable comments that are "author visible". This especially applies to comments in the "submission" thread, because...
### Is your feature request related to a problem? According to https://github.com/rocq-prover/rocq/issues/6093 it is the case since Rocq 9.0 that "template polymorphism can be seen as an optimization of universe...