Skip to content

Remove old `Hint Extern` hack for `impl_persistent` that seems no longer needed.

Robbert Krebbers requested to merge ci/robbert/hint_extern_impl_persistent into master

I think this hack was needed for older versions of Coq, but it seems no longer be necessary. I added some tests to make sure that the instance is actually found.

Merge request reports