Applying François Garillot's patch (#2261 in bug tracker) for extended

syntax of "Implicit Type" (that can now be "Implicit Types" and can
now accept several blocks of variables of a given type).

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

1 files changed, 2 insertions, 0 deletions

diff --git a/CHANGES b/CHANGES
index 63900a2b76..eb906205e9 100644
--- a/CHANGES
+++ b/CHANGES
@@ -163,6 +163,8 @@ Vernacular commands
   variables before the colon at the start of interactive proofs.
 - New command "Declare Reduction <id> := <conv_expr>", allowing to write
   later "Eval <id> in ...". This command accepts a Local variant.
+- Syntax of Implicit Type now supports more than one block of variables of
+  a given type.
 
 Library