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
[x] Declare Scope
Coq >= 8.12
[x] Add #[export] attribute to hints (in the meantime we can put Global everywhere to silence warnings)
Coq >= 8.13
[x] 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. (#227 WIP)
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 ScopeCoq >= 8.12
#[export]attribute to hints (in the meantime we can putGlobaleverywhere to silence warnings)Coq >= 8.13
identwithname(ITreeDefinition.v...)Coq >= 8.14
#[global]to#[extern]on instances and hints. Figure out what should be re-exported. (#227 WIP)