The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 08/19/2016 10:26 PM, Jonathan Leivent wrote:
> ...
> OK - maybe it wouldn't be so hard to fix the standard library and 
> plugins after all...

I tried this typeclasses replacement of axioms in part of a development 
I have that contains its own axiom.  It requires a bit more care and 
feeding than I anticipated, but there do seem to be workarounds for the 
various issues that arise (such as the addition of an implicit arg on 
each definition that consumes axioms). Unfortunately, its the kind of 
work that probably means a change like this would not be considered a 
drop-in replacement for the existing axioms in the standard library.

-- Jonathan