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.

---
 interp/constrexpr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrexpr.ml')

diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml
index c98e05370e..bfdee7c50d 100644
--- a/interp/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -108,7 +108,7 @@ and constr_expr_r =
          * constr_expr * constr_expr
   | CHole   of Evar_kinds.t option * Namegen.intro_pattern_naming_expr * Genarg.raw_generic_argument option
   | CPatVar of Pattern.patvar
-  | CEvar   of Glob_term.existential_name * (Id.t * constr_expr) list
+  | CEvar   of Glob_term.existential_name * (lident * constr_expr) list
   | CSort   of Glob_term.glob_sort
   | CCast   of constr_expr * constr_expr Glob_term.cast_type
   | CNotation of notation_with_optional_scope option * notation * constr_notation_substitution
-- 
cgit v1.2.3