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_term.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/glob_term.ml')

diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 526eac6f1e..04e9382015 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -75,7 +75,7 @@ type 'a glob_constr_r =
   | GVar of Id.t
       (** An identifier that cannot be regarded as "GRef".
           Bound variables are typically represented this way. *)
-  | GEvar   of existential_name * (Id.t * 'a glob_constr_g) list
+  | GEvar   of existential_name * (lident * 'a glob_constr_g) list
   | GPatVar of Evar_kinds.matching_var_kind (** Used for patterns only *)
   | GApp    of 'a glob_constr_g * 'a glob_constr_g list
   | GLambda of Name.t * binding_kind *  'a glob_constr_g * 'a glob_constr_g
-- 
cgit v1.2.3