From dce9fe9bd4cab3e560f41a8d7cbf447b27665e1f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 13 Sep 2009 13:24:21 +0000
Subject: - Inductive types in the "using" option of auto/eauto/firstorder are 
  interpreted as using the collection of their constructors as hints. - Add
 support for both "using" and "with" in "firstorder". Made the   syntax of
 "using" compatible with the one of "auto" by separating   lemmas by commas.
 Did not fully merge the syntax: auto accepts   constr while firstorder
 accepts names (but are constr really useful?). - Added "Reserved Infix" as a
 specific shortcut of the corresponding   "Reserved Notation".

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index b02988c8aa..3a471e9478 100644
--- a/CHANGES
+++ b/CHANGES
@@ -32,6 +32,10 @@ Tactics
 - Tactic "exists" and "eexists" supports iteration using
   comma-separated arguments.
 - Tactic "gappa" has been removed from the Dp plugin.
+- Tactic "firstorder" now supports the combination of its "using" and
+  "with" options.
+- An inductive type as argument of the "using" option of "auto/eauto/firstorder"
+  is interpreted as using the collection of its constructors.
 
 Tactic Language
 
@@ -45,6 +49,8 @@ Vernacular commands
 - New support for local binders in the syntax of Record/Structure fields.
 - Most commands referring to constant (e.g. Print or About) now support
   referring to the constant by a notation string.
+- Added "Reserved Infix" as a specific shortcut of the corresponding
+  "Reserved Notation".
 
 Tools
 
-- 
cgit v1.2.3