diff options
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 74263b768..00aa7fb6c 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -494,7 +494,7 @@ let make_notation_key symbols = let decompose_notation_key s = let len = String.length s in let rec decomp_ntn dirs n = - if n>=len then dirs else + if n>=len then List.rev dirs else let pos = try String.index_from s n ' ' |