Fixing another bug with "_" intro pattern.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14185 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 1 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index bf4673909a..80111bc986 100644
--- a/CHANGES
+++ b/CHANGES
@@ -29,6 +29,7 @@ Tactics
   in scripts meant to be machine-independent.
 - Fixing a bug of destruct that left local definitions in context might result
   in some rare incompatibilities (solvable by adapting name hypotheses).
+- Introduction pattern "_" made more robust.
 - Tactic (and Eval command) vm_compute can now be interrupted via Ctrl-C.
 
 Vernacular commands