Des critères plus fins d'analyse des implicites automatiques; meilleur affichage des implicites en cas d'application partielle ou inférence via une position flexible; gestion des implicites en positions terminales pour anticiper sur un implicite dans nil et cie

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

1 files changed, 7 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index eb0738d116..0900445c97 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,10 +1,17 @@
 Changes from V7.3.1 to ????
 -------------------------
 
+TODO: unification 2eme ordre avec NewDestruct
+
 Symbolic notations
 
 - Introduction of a notion of scope gathering notations in a consistent set;
   set a notation sets has been developped for nat, Z and R
+- Declarations with only implicit arguments now handled (e.g. the
+  argument of nil can be set implicit; use !nil to refer to nil
+  without arguments)
+- New defensive strategy for printing or not implicit arguments to ensure
+  re-type-checkability of the printed term
 
 Library