diff options
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index 57553f9e1a..bf4e6dedde 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -24,6 +24,14 @@ Universe Polymorphism. (e.g. induction). Extra "Transparent" might have to be added to revert opacity of constants. +Records, Classes. + +- The generated binder name of the class argument of projections + in type class declarations is now the same as for the corresponding + record name and is the lowercase first character of the class name. + E.g for [Class Foo (A : Type) := foo : A -> A], foo's class argument + has name [f]. + Potential sources of incompatibilities between Coq V8.3 and V8.4 ---------------------------------------------------------------- |