Fix w.r.t. coq/coq#14876.

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]

https://math-classes.github.io

MIT License

160 stars 43 forks source link

Fix w.r.t. coq/coq#14876. #104

Closed ppedrot closed 3 years ago

Zimmi48 commented 3 years ago

Why is this a draft PR?

ppedrot commented 3 years ago

Because it shouldn't merged yet. It's likely to be backwards compatible but I have to think a bit if the new behaviour of Hint Unfold is really the desired one.