Compatibility fixes

[Lysxia]

Interaction Trees tries to remain buildable with old versions of Coq (currently back to 8.9) until it's too much of a hassle. Here's a (likely partial) list of fixes that should happen once too old versions are dropped:

• Coq >= 8.10

  • Declare Scope

• Coq >= 8.12

  • Add #[export] attribute to hints (in the meantime we can put Global everywhere to silence warnings)

• Coq >= 8.13

  • In notations, replace entry ident with name (ITreeDefinition.v...)

• Coq >= 8.14

  • Change #[global] to #[extern] on instances and hints. Figure out what should be re-exported. (Add #[global] attribute to Hint Rewrite #227 WIP)