From e2da4d5758d0167cb621f2b57bb61708a2d6dbe4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 4 Dec 2012 23:26:21 +0000
Subject: Revised the strategy for automatic insertion of spaces when printing
 notations: - hopefully never 2 spaces when the user did not ask for - more
 systematic default insertion of spaces around symbols - e.g. have space
 before "[" if after a non-terminal - have spaces between consecutive
 terminals

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

(limited to 'CHANGES')

diff --git a/CHANGES b/CHANGES
index 3fd784affe..a8de063188 100644
--- a/CHANGES
+++ b/CHANGES
@@ -40,6 +40,8 @@ Notations
 - 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.
+- More systematic insertion of spaces as a default for printing
+  notations ("format" still available to override the default).
 
 Internal Infrastructure
 
-- 
cgit v1.2.3