Typeclasses eauto

[FissoreD]

Typeclasses eauto leaves a sealed goal in the resolution of a class instead of failing.

• [ ] Pass the eauto flag to the resolution process
• [ ] Add a clause before solve-aux-fail to return [seal G] if eauto is active

[FissoreD]

This seems to be solved by Coq PR19148 and Coq-elpi PR635

Before closing the issue, I want branch tc_register_in_coq merged into branch ho-unif-with-links-new.

This needs some rebasing work...