From f77d428c11bf47c20b8ea67d8ed7dce6af106bcd Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 22 Apr 2010 13:51:03 +0000 Subject: 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 --- CHANGES | 2 ++ 1 file changed, 2 insertions(+) (limited to 'CHANGES') 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 := ", allowing to write later "Eval in ...". This command accepts a Local variant. +- Syntax of Implicit Type now supports more than one block of variables of + a given type. Library -- cgit v1.2.3