aboutsummaryrefslogtreecommitdiff
path: root/CHANGES.md
diff options
context:
space:
mode:
Diffstat (limited to 'CHANGES.md')
-rw-r--r--CHANGES.md4
1 files changed, 4 insertions, 0 deletions
diff --git a/CHANGES.md b/CHANGES.md
index 6bdb63d4d7..5ff90b5123 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -120,6 +120,10 @@ Universes
- Added `Print Universes Subgraph` variant of `Print Universes`.
Try for instance `Print Universes Subgraph(sigT2.u1 sigT_of_sigT2.u1 projT3_eq.u1 eq_sigT2_rect.u1).`
+Misc
+
+- Option "Typeclasses Axioms Are Instances" is deprecated. Use Declare Instance for axioms which should be instances.
+
Changes from 8.8.2 to 8.9+beta1
===============================