use Coq's elaborator for factories and instances

[gares]

That's it.
It requires a non released version of Coq-Elpi (including PR LPCIC/coq-elpi#170). It would be nice if it we could give it a try on mathcomp before releasing Coq-Elpi 1.6 (so that we are sure we don't miss something in LPCIC/coq-elpi#170).

Depends on LPCIC/coq-elpi#170 it was tested locally and works, here CI does not pick up the needed Coq-Elpi branch.
Fix #98 #34

[gares]

I move this PR on top of PR #108 and tried it onhttps://github.com/gares/math-comp/tree/hierarchy-builder. Result:
gares/math-comp@1e15970

The only thing that looks fishy is that HB.instance term1 term2 does not elaborate term1 as a type (so coercions to Typeclass are not inserted). In this specific case it may even be a feature, since you are forced to make the key sub_sort explicit, but in general it sucks. We may solve this API problem by having both argument->term and argument->type, but I don't know if we really want it for HB.instance first argument.

[gares]

Depends on rocq-prover/opam#1392

[gares]

@CohenCyril it works

[gares]

After this rocq-prover/opam#1397 we can revert the HACK and merge (opam should work on both 8.11 and 8.12). For nix, what should we do @CohenCyril ?

[CohenCyril]

we can revert the HACK

Can you refresh my memory about the nature of "the HACK" at hand?

[gares]

For some reasons the 2 jobs are linked, and if 8.11 fails then the 8.12 is cancelled. Since there was no 8.11 version of Coq-Elpi 1.6, that job was immediately failing.

[gares]

OK, opam is good. If we merge master is back working on both 8.11 and 8.12