Release notes for Agda version 2.6.3
Added support for Erased Cubical Agda, a variant of Cubical Agda that is supported by the GHC backend, under the flag --erased-cubical.
Added a new flag --cubical-compatible to turn on generation of Cubical Agda-specific support code (previously this behaviour was part of --without-K).
Since --cubical-compatible mode implies that functions should work with the preliminary support for indexed inductive types in Cubical Agda, many pattern matching functions will now emit an UnsupportedIndexedMatch warning, indicating that the function will not compute when applied to transports (from --cubical code).
This warning can be disabled with -WnoUnsupportedIndexedMatch, which can be used either in an OPTIONS pragma or in your agda-lib file. The latter is recommended if your project is only --cubical-compatible, or if it is already making extensive use of indexed types.
Note that code that uses (only) --without-K can no longer be imported from code that uses --cubical. Thus it may make sense to replace --without-K with --cubical-compatible in library code, if possible.
