aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/metasyntax.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 92208e304..4f41043e8 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1203,7 +1203,10 @@ let contract_notation ntn =
let rec aux ntn i =
if i <= String.length ntn - 5 then
let ntn' =
- if String.is_sub "{ _ }" ntn i then
+ if String.is_sub "{ _ }" ntn i &&
+ (i = 0 || ntn.[i-1] = ' ') &&
+ (i = String.length ntn - 5 || ntn.[i+5] = ' ')
+ then
String.sub ntn 0 i ^ "_" ^
String.sub ntn (i+5) (String.length ntn -i-5)
else ntn in