diff options
| author | Matthieu Sozeau | 2014-10-11 12:11:07 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-10-11 12:15:49 +0200 |
| commit | d4b3de96f524887013c0955bd5b90f0311f086e6 (patch) | |
| tree | ea87e31c9c4681911c9dede29de2d1b51a86deec /COMPATIBILITY | |
| parent | d65496f09c4b68fa318783e53f9cd6d5c18e1eb7 (diff) | |
Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different name
for the record binder of classes. This name is no longer generated
in the kernel but part of the declaration. Also cleanup the interface
to recognize primitive records based on an option type instead of a
dynamic check of the length of an array.
Diffstat (limited to 'COMPATIBILITY')
| -rw-r--r-- | COMPATIBILITY | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/COMPATIBILITY b/COMPATIBILITY index bf4e6dedde..57553f9e1a 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -24,14 +24,6 @@ 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 ---------------------------------------------------------------- |