aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrexpr_ops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrexpr_ops.ml')
-rw-r--r--interp/constrexpr_ops.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 950edc5a3..306fbfad9 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -75,7 +75,7 @@ let local_binder_loc = function
let local_binders_loc bll =
if bll = [] then Loc.ghost else
- Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (list_last bll))
+ Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (List.last bll))
(** Pseudo-constructors *)