diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-10 18:54:56 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-10 21:23:01 +0200 |
| commit | d0cd27e209be08ee51a2d609157367f053438a10 (patch) | |
| tree | 29c4f71268ab5cab9e6615732c66107ac1c84a71 /COMPATIBILITY | |
| parent | 8a9de08c0e6a5130103cedf05cbcebcf5f621d1e (diff) | |
Give the same argument name for the record binder of type class
projections and regular records.
Easily fixable backwards incompatibility.
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index 57553f9e1..bf4e6dedd 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 ---------------------------------------------------------------- |