From 26b9ad1d0423f8dc1dbd4d90557469db6a5eaa03 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 18 Sep 2017 19:00:09 +0200 Subject: Fixing two anomalies in corner cases of the syntax of notation formats. --- vernac/metasyntax.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac/metasyntax.ml') diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index c424b1d50..3126b1b14 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -129,12 +129,12 @@ let parse_format ((loc, str) : lstring) = and parse_quoted n i = if i < len then match str.[i] with (* Parse " // " *) - | '/' when i <= len && str.[i+1] == '/' -> - (* We forget the useless n spaces... *) + | '/' when i+1 < len && str.[i+1] == '/' -> + (* We discard the useless n spaces... *) push_token (UnpCut PpFnl) (parse_token 1 (close_quotation (i+2))) (* Parse " .. / .. " *) - | '/' when i <= len -> + | '/' when i+1 < len -> let p = spaces 0 (i+1) in push_token (UnpCut (PpBrk (n,p))) (parse_token 1 (close_quotation (i+p+1))) -- cgit v1.2.3