diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 17:30:37 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-07-05 17:30:37 +0000 |
commit | afe903e7889625986edab5506e3bb2cb90f7f483 (patch) | |
tree | 3e03b9273b837502aa0f1fb6b197519370bb0235 /theories/QArith | |
parent | 819029226c334030a540ed7570bc423c4463c6b4 (diff) |
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
Diffstat (limited to 'theories/QArith')
0 files changed, 0 insertions, 0 deletions