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.