From 41e36fe75b0859480c523e40361b75a13afcfe69 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 9 Jun 2010 12:52:04 +0000 Subject: Keep description of Automatic Introduction at only one place of CHANGES. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13100 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 2 -- 1 file changed, 2 deletions(-) diff --git a/CHANGES b/CHANGES index 0aef24b87..128b3dafb 100644 --- a/CHANGES +++ b/CHANGES @@ -168,8 +168,6 @@ Vernacular commands - New command "Print Opaque Dependencies" to display opaque constants in addition to all variables, parameters or axioms a theorem or definition relies on. -- New option [Set Automatic Introduction] to automatically introduce - 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 -- cgit v1.2.3