# HG changeset patch
# User wenzelm
# Date 1186938058 -7200
# Node ID 4714e04fb8e9d57c650494691fd59a3ad452d9fb
# Parent  5bec1b4149e7fc8dbb49a5f2236c92d0e4bae89c
* Syntax: scope for resolving ambiguities via type-inference is now limited to individual terms;

diff -r 5bec1b4149e7 -r 4714e04fb8e9 NEWS
--- a/NEWS	Sun Aug 12 18:53:05 2007 +0200
+++ b/NEWS	Sun Aug 12 19:00:58 2007 +0200
@@ -46,6 +46,13 @@
 feature, which will disappear eventually. Even now, the theory loader no
 longer maintains dependencies on such files.
 
+* Syntax: the scope for resolving ambiguities via type-inference is now
+limited to individual terms, instead of whole simultaneous
+specifications as before. This greatly reduces the complexity of the
+syntax module and improves flexibility by separating parsing and
+type-checking. INCOMPATIBILITY: additional type-constraints (explicit
+'fixes' etc.) are required in rare situations.
+
 * Legacy goal package: reduced interface to the bare minimum required
 to keep existing proof scripts running.  Most other user-level
 functions are now part of the OldGoals structure, which is *not* open