From cb0dea2a0c2993d4ca7747afc61fecdbb1c525b1 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 30 Jul 2015 19:20:39 +0200
Subject: Documenting change of behavior of apply when the lemma is a tuple and
 applying a component of the tuple.

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

diff --git a/CHANGES b/CHANGES
index 733bcc7cf5..2e5e30ef8d 100644
--- a/CHANGES
+++ b/CHANGES
@@ -35,7 +35,6 @@ API
   * A new safe pf_type_of function.
   All uses of unsafe_* functions should be eventually eliminated.
 
-
 Tools
 
 - Added an option -w to control the output of coqtop warnings.
@@ -359,6 +358,10 @@ Tactics
   trace anymore. Use "Info 1 auto" instead. The same goes for
   "info_trivial". On the other hand "info_eauto" still works fine,
   while "Info 1 eauto" prints a trivial trace.
+- When using a lemma of the prototypical form "forall A, {a:A & P a}",
+  "apply" and "apply in" do not instantiate anymore "A" with the
+  current goal and use "a" as the proof, as they were sometimes doing,
+  now considering that it is a too powerful decision.
 
 Program
 
-- 
cgit v1.2.3