From d0cd27e209be08ee51a2d609157367f053438a10 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Fri, 10 Oct 2014 18:54:56 +0200
Subject: Give the same argument name for the record binder of type class
 projections and regular records. Easily fixable backwards incompatibility.

---
 COMPATIBILITY | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'COMPATIBILITY')

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
 ----------------------------------------------------------------
 
-- 
cgit v1.2.3