search

coq-community / math-classes

A library of abstract interfaces for mathematical structures in Coq [maintainer=@spitters,@Lysxia]
https://math-classes.github.io
MIT License
162 stars 43 forks source link

math-classes relies on deprecated `Set Automatic Coercions Import` #55

Closed maximedenes closed 6 years ago

maximedenes commented 6 years ago

This option has been marked as deprecated for some time now, I'd lilke to remove it from Coq (see https://github.com/coq/coq/pull/8094 for context).

Could math-classes be adapted to not use this option?

maximedenes commented 6 years ago

More generally, there are quite a few warnings shown when building math-classes (I hope I'm not mixing up with Corn). I believe they should be addressed, so that we can clean things up on the Coq side.

spitters commented 6 years ago

I'd like to clean that up, but I'm really pressed for time at the moment. Maybe this could be part where the new coq-community could be helpful in maintaining?

Zimmi48 commented 6 years ago

We could try to use standard "help wanted" label recommended by GitHub and encourage people to address these issues from the coq-community homepage / main repo.

maximedenes commented 6 years ago

I'm going to give it a try, for this particular warning, but help is wanted for other deprecation warnings indeed.

Zimmi48 commented 6 years ago

Fixed by #58. We should probably have a new issue, labeled "help wanted" for other warnings.