implicites manuels

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

1 files changed, 10 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index b5d85ac15..db1ef0b33 100644
--- a/CHANGES
+++ b/CHANGES
@@ -57,6 +57,16 @@ que les 3 primitives), on peut typer avec "constr", "tactic", ou
   Begin Silent -> Set Silent
   End Silent -> Unset Silent.
 
+- Déclaration manuelle des implicites avec
+
+	Implicits ident.
+	Implicits ident [ num num ... num ].
+
+  Petit changement de sémantique : lors de la fermeture d'une section,
+  les implicites sont calculés selon la valeur *courante* de "Implicit 
+  Arguments" et non plus selon la valeur qu'elle avait au moment de la 
+  définition dans la section.
+
 Tactiques
 
 - Langage de tactique