From 9105a72e3d39e482c9e078de9f71efafc6cc3d0f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 11 Nov 2014 13:29:10 +0100
Subject: Updating CHANGES (evars as ident).

---
 CHANGES | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/CHANGES b/CHANGES
index ad6399bc77..8aa42bb63d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -77,6 +77,10 @@ Specification Language
 - Type inference algorithm now granting opacity of constants. This might also
   affects behavior of tactics (source of incompatibilities, solvable by
   re-declaring transparent constants which were set opaque).
+- Existential variables are now referred to by an identifier and the
+  relevant part of their instance is displayed by default. They can be
+  reparsed. The naming policy is yet unstable and subject to changes
+  in future releases.
 
 Tactics
 
-- 
cgit v1.2.3