Skip to content

Take advantage of new Coq features in Coq 8.15

Robbert Krebbers requested to merge robbert/coq815 into master
  • #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.

Edited by Robbert Krebbers

Merge request reports