Take advantage of new Coq features in Coq 8.15

• #7725 (8.15): Allows overriding intuition_solver instead of shadowing [intuition], see also #143
• #14513 (8.15): Allow Global on Typeclasses Opaque/Transparent and Hint Mode, inside sections.
• #13952 (8.15): Use hint ! for Equiv type class.
• 8.15: #[projections(primitive=yes/no)] for better primitive projection control.

Also I removed an obsolete comment about omega, which has been removed since Coq 8.14.

added 11 commits

• 8d123328...22151b7b - 5 commits from branch master
• 59af581a - Remove obsolete remark, `omega` has been removed in Coq 8.14.
• 0b4d25e7 - Use `#[projections(primitive=yes)]` pragma.
• c1c542a0 - Override `intuition_solver` instead of redeclaring `intuition`.
• 8574b623 - Add `Global` to `Typeclasses Opaque`/`Typeclasses Transparent`.
• 9fddc01a - Set `Hint Mode` for `Equiv`.
• b8561191 - CHANGELOG.

Compare with previous version

This MR now also includes the relevant part of !437 (closed), i.e., set Hint Mode Equiv !.

I also included a CHANGELOG.

Setting Hint Equiv is a breaking change, reverse dependencies might have ambiguous uses of ≡ and those need to be fixed.

Allow Global on Typeclasses Opaque/Transparent and Hint Mode, inside sections.

Hint Mode was already supporting Global before I think? At least our linter enforced it...

added 1 commit

• 11113899 - coq-lint: enforce TC opaque having locality annotations

Compare with previous version

Allow Global on Typeclasses Opaque/Transparent and Hint Mode, inside sections.

I extended coq-lint to enforce locality on all of these, let's see what CI says.

mentioned in merge request !437 (closed)

changed the description

resolved all threads

CI succeeds, so that seems we obey to @jung's linter script.

merged

mentioned in commit 1f83a259

@iris-users

• Set Hint Mode Equiv !; this might need some type annotations for ambiguous uses of ≡.
• Set intuition_solver ::= auto (the default is auto with *) instead of redeclaring intuition.

mentioned in issue #138 (closed)