From afe903e7889625986edab5506e3bb2cb90f7f483 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 5 Jul 2012 17:30:37 +0000
Subject: Quick update to CHANGES, mention especially the new parsing of ->

 So -> is at level 99 since commit 15515. In particular it has now
 *less* priority than <->, i.e. A->B<->C is now parsed as A->(B<->C)
 instead of the former awkward and beginner-misleading (A->B)<->C.
 Sorry, I was planning to do a separate commit for that, but I forgot.
 In fact, the parsing rules for -> were slightly changed during
 Pierre B's recent conversion of -> to a true Notation, leading
 to a nasty sitution : A->B<->C->D was parsed as A->(B<->(C->D)).
 With no obvious solution to restore full compatibility, we decided
 to go for the parsing described above, both easy to implement
 and to work with.

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

diff --git a/CHANGES b/CHANGES
index b0b067e682..0819cdeede 100644
--- a/CHANGES
+++ b/CHANGES
@@ -7,6 +7,12 @@ Vernacular commands
   (foo_rect, foo_rec, foo_ind) anymore by default (feature wish #2693).
   A flag "Set/Unset Record Elimination Schemes" allows to change this.
   The tactic "induction" on a record is now actually doing "destruct".
+- The "Open Scope" command can now be given also a delimiter (e.g. Z).
+
+Specification Language
+
+- The syntax "x -> y" is now declared at level 99. In particular, it has
+  now a lower priority than "<->" : "A -> B <-> C" is now "A -> (B <-> C)".
 
 Tactics
 
@@ -29,6 +35,9 @@ Program
 Notations
 
 - "Bind Scope" can no longer bind "Funclass" and "Sortclass".
+- A notation can be given a (compat "8.x") annotation, making
+  it behave like a (only parsing), but flags may active warning
+  or error when this notation is used.
 
 Internal Infrastructure
 
-- 
cgit v1.2.3