From e660d5466bcea7e996a9dce85f37c1280d83097e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 17 Mar 2004 13:35:58 +0000
Subject: MAJ

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

diff --git a/CHANGES b/CHANGES
index b020256ce4..cdedac16e1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -8,21 +8,19 @@ Commands
   if-then-else, notations, projections)
 - "Functional Scheme" and "Functional Induction" extended to polymorphic types
   and dependent types
-
-Syntax
-
+- Notation now allows recursive patterns, hence recovering parts of V7 Grammar
+  fonctionalities
 - Command "Print." discontinued.
-- "assert" semantics now consistent with reference manual
 - Redundant syntax "Implicit Arguments On/Off" discontinued
-- Delimiting key %bool for bool_scope added
 
 Interpretation scopes
 
-- Add scope %bool
+- Delimiting key %bool for bool_scope added
 - Import no more needed to activate argument scopes from a module
 
 Tactics
 
+- "assert" semantics now consistent with reference manual
 - New tactics stepl and stepr for chaining transitivity steps
 - Tactic "replace ... with ... in" added
 
-- 
cgit v1.2.3