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...

`Set Typeclasses Unique Instances` does not seem to be working

40

#### 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...

Rename Coq module from diris into cgraphs

1

The name `diris` was still there for legacy purposes, it should be consistent with the name of the repo.

Make clear what versions of Coq are supported

2

This information is not in the README. I think it would be good to include it there.

Make work with recent versions of Coq

1

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...

Attribute for `Unset Elimination Schemes`

2

### 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...

Spurious "incompatible prefixes" warning for "printing only" notations

2

### 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...