From 7fd28dc95e3251a10617ddb6758cc00b8960f954 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Mar 2018 13:19:13 +0100
Subject: Slightly refining some error messages about unresolvable evars.

For instance, error in "Goal forall a f, f a = 0" is now located.
---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/cases.ml')

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a5b7a9e6f0..73be9d6b78 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1662,7 +1662,7 @@ let rec list_assoc_in_triple x = function
 let abstract_tycon ?loc env evdref subst tycon extenv t =
   let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*)
   let src = match EConstr.kind !evdref t with
-    | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk)
+    | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar (None,evk))
     | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in
   let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv !evdref subst t in
   (* We traverse the type T of the original problem Xi looking for subterms
-- 
cgit v1.2.3