<!-- Thank you for reporting a bug to Coq! -->

#### Description of the problem

<!-- If you can, it's helpful to provide self-contained example of some code
that reproduces the bug. If not, a link to a larger example is also helpful.
You can generate a shorter version of your program by following these
instructions: https://github.com/coq/coq/wiki/Coqbot-minimize-feature.  -->

#### Coq Version

<!-- You can get this information by running `coqtop -v`. If relevant, please
also include your operating system. -->