From 2c8335b4d2cf928f8494b4abf100b5bb6a8d2fa0 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 27 Jun 2014 11:28:35 +0200
Subject: Updating CHANGES w.r.t. opacity in type inference + layout of file.

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

(limited to 'COMPATIBILITY')

diff --git a/COMPATIBILITY b/COMPATIBILITY
index 33bb1d30ee..57553f9e1a 100644
--- a/COMPATIBILITY
+++ b/COMPATIBILITY
@@ -19,6 +19,11 @@ Universe Polymorphism.
   An explicit parameter application (e.g [fun A => list A]) or
   [apply (list _)] will result in a polymorphic instance.
 
+- The type inference algorithm now takes opacity of constants into
+  account. This may have effects on tactics using type inference
+  (e.g. induction). Extra "Transparent" might have to be added to
+  revert opacity of constants.
+
 Potential sources of incompatibilities between Coq V8.3 and V8.4
 ----------------------------------------------------------------
 
-- 
cgit v1.2.3