Broken in Coq CI

[SkySkimmer]

eg https://gitlab.inria.fr/coq/coq/-/jobs/5319611 https://gitlab.inria.fr/coq/coq/-/jobs/5320146

Probably due to math-comp/hierarchy-builder#514 (cc @proux01) considering it's the difference between recent success https://gitlab.inria.fr/coq/coq/-/jobs/5319341 and the failures AFAICT

[proux01]

Might be the case, jasmin is unfortunately one of the few missing thing in CI there (it's not in nixpkgs IIRC).
The good news is that it's probably just a missing requrie Strings or something in jasmin that was silently relying on HB exporting it, so should be fairly easy to fix for jasmin devs.

[proux01]

The relevant part of the diff there seems to be

- From Coq Require Import String.
- Export String.StringSyntax.
- Global Open Scope string_scope.

(c.f. HB/structures.v in https://github.com/math-comp/hierarchy-builder/pull/514/files )

[vbgl]

Thanks for reporting and investigating the issue.

[vbgl]

Reproduced: https://gitlab.com/jasmin-lang/jasmin/-/jobs/9118451101#L8350