Continuing r12485-12486 and r12549 (cleaning around name generation)

- fixed misunderstanding of the role of nenv while simplifying code of
  occur_id in namegen.ml,
- documented the possible incompatibilites in CHANGES
- fixed output/Naming.v test, and fixed the count of misc. tests in
  test-suite/check.

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

1 files changed, 3 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 627408cc88..0a6ee0d9f9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -45,6 +45,9 @@ Tactics
 - Binders given before ":" in lemmas are now automatically
   introduced in the context (possible source of incompatibility that can be
   avoided by unsetting option "Automatic Introduction").
+- Made choice of introduction names compliant with printed names and
+  in particular with "intros until" names (possible source of exceptional
+  incompatibilities).
 
 Tactic Language