aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--interp/topconstr.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index b043f3d423..97f9429c17 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -262,8 +262,8 @@ let locs_of_notation loc locs ntn =
let (bl, el) = Loc.unloc loc in
let locs = List.map Loc.unloc locs in
let rec aux pos = function
- | [] -> if Int.equal pos el then [] else [(pos,el-1)]
- | (ba,ea)::l ->if Int.equal pos ba then aux ea l else (pos,ba-1)::aux ea l
+ | [] -> if Int.equal pos el then [] else [(pos,el)]
+ | (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l
in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs)
let ntn_loc loc (args,argslist,binderslist) =