aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/metasyntax.ml
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-04-29 12:02:24 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-04-29 12:02:24 +0000
commit4b9070eefcdb135226fb4f3c2706519796b0284e (patch)
treed850494ca090fbd96850321f16055050b8d36d76 /toplevel/metasyntax.ml
parent9a245295665681af621688ab924093f451ec340c (diff)
Moins de ' ' à l'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3973 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/metasyntax.ml')
-rw-r--r--toplevel/metasyntax.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index ece8acb2b..51a9eec35 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -336,10 +336,10 @@ let make_hunks etyps symbols from =
else
UnpTerminal s :: add_break 1 (make NoBreak prods)
else
- if ws = CanBreak then
+ if ws = CanBreak or is_ident_tail s.[String.length s - 1] then
add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods)
else
- UnpTerminal (s^" ") :: make CanBreak prods
+ UnpTerminal s :: make CanBreak prods
| Terminal s :: prods ->
if is_right_bracket s then