Fixed notation printing bug when curly brackets are involved (requests

for adding spaces were not taken into account in notations containing
patterns of the form "{ ident symbol", paradoxically resulting in
adding extra spaces, e.g. when printing the type "{ x |  P x }" of
"exist", due to interferences with the heuristic for adding breaking
points in Metasyntax.make_hunk).

Also adapted output of test InitSyntax.v after commit r14018 improved
the printing of "ex P" and "sig P".

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14073 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions