aboutsummaryrefslogtreecommitdiff
path: root/interp/constrexpr_ops.ml
diff options
context:
space:
mode:
authorHugo Herbelin2020-04-27 14:39:56 +0200
committerHugo Herbelin2020-10-10 22:13:59 +0200
commit2cf0287c9c863d7969fb5d4e85b7ca538dd103c2 (patch)
tree0dfa98a20514443017dcd81d165cdcb494e5743f /interp/constrexpr_ops.ml
parent03d55f990bb7a2c4f5c1fefa408b94a8a93e8d05 (diff)
Adding and using locations on identifiers in constr_expr where they were missing.
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 ce8e7d3c2c..3400485ad5 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -235,7 +235,7 @@ and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
List.equal (List.equal local_binder_eq) bl1 bl2
and instance_eq (x1,c1) (x2,c2) =
- Id.equal x1 x2 && constr_expr_eq c1 c2
+ Id.equal x1.CAst.v x2.CAst.v && constr_expr_eq c1 c2
and cast_expr_eq c1 c2 = match c1, c2 with
| CastConv t1, CastConv t2