From 2cf0287c9c863d7969fb5d4e85b7ca538dd103c2 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 27 Apr 2020 14:39:56 +0200
Subject: Adding and using locations on identifiers in constr_expr where they
 were missing.

---
 pretyping/glob_ops.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/glob_ops.ml')

diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 5bd26be823..fd6083abd1 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -128,7 +128,7 @@ let fix_kind_eq k1 k2 = match k1, k2 with
   | (GFix _ | GCoFix _), _ -> false
 
 let instance_eq f (x1,c1) (x2,c2) =
-  Id.equal x1 x2 && f c1 c2
+  Id.equal x1.CAst.v x2.CAst.v && f c1 c2
 
 let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
   | GRef (gr1, u1), GRef (gr2, u2) ->
-- 
cgit v1.2.3