diff --git a/CHANGELOG.md b/CHANGELOG.md index 0c19f8792b17a0332b0967710a50f8a92db5c7fb..607fdf3d9218bbec8a0d23bd0c8950d49eb250c8 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -31,6 +31,8 @@ Coq 8.11 is no longer supported in this version of Iris. `Dist`, `Op`, `Valid`, `ValidN`, `Unit`, `PCore` now use an `Hint Extern` based on `refine` instead of `apply`, in order to use Coq's newer unification algorithm. +* Set `Hint Mode` for the classes `OfeDiscrete`, `Unit`, `CmraMorphism`, + `rFunctorContractive`, `urFunctorContractive`. **Changes in `bi`:**