diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-18 19:00:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-09-18 19:05:16 +0200 |
| commit | 26b9ad1d0423f8dc1dbd4d90557469db6a5eaa03 (patch) | |
| tree | c74f30f4f8aa2b42c0990ec98d37ef448e8b26b2 /vernac/metasyntax.ml | |
| parent | 296941dc97d53817cc58b4687ed99168e1dd33a9 (diff) | |
Fixing two anomalies in corner cases of the syntax of notation formats.
Diffstat (limited to 'vernac/metasyntax.ml')
| -rw-r--r-- | vernac/metasyntax.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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))) |