From e60054fe4dbdc26ed545c7ca6fb8ab36b244f2f7 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Oct 2008 11:38:47 +0000
Subject: - Fixed many "Theorem with" bugs. - Fixed doc of assert as. - Doc of
 apply in + update credits. - Nettoyage partiel de Even.v en utilisant
 "Theorem with". - Added check that name is not in use for "generalize as".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11511 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 CHANGES | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 326ac272e7..72dd724325 100644
--- a/CHANGES
+++ b/CHANGES
@@ -243,6 +243,7 @@ Tactics
   to remember the term to which the induction or case analysis applied
   (possible source of parsing incompatibilities when destruct or induction is
    part of a let-in expression in Ltac; extra parentheses are then required).
+- New support for "as" clause in tactics "apply in" and "eapply in".
 - Some new intro patterns: 
   * intro pattern "?A" genererates a fresh name based on A. 
     Caveat about a slight loss of compatibility:
@@ -285,7 +286,7 @@ Tactics
 - Tactic firstorder "with" and "using" options have their meaning swapped for
   consistency with auto/eauto (source of incompatibility).
 - Tactic "generalize" now supports "at" options to specify occurrences
-  and "as" options to name the hypothesis.
+  and "as" options to name the quantified hypotheses.
 - New tactic "specialize H with a" or "specialize (H a)" allows to transform
   in-place a universally-quantified hypothesis (H : forall x, T x) into its 
   instantiated form (H : T a). Nota: "specialize" was in fact there in earlier
-- 
cgit v1.2.3