From b39465da31bfd488dfad4ea4627186f9a1843e56 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 23 Oct 2014 20:38:44 +0200
Subject: VarInstance are also goals.

---
 proofs/proofview.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 569ae148ae..d69ee0260b 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -888,7 +888,9 @@ struct
   let mark_as_goal evd content =
     let info = Evd.find evd content in
     let info =
-      { info with Evd.evar_source = (fst (info.Evd.evar_source),Evar_kinds.GoalEvar) }
+      { info with Evd.evar_source = match info.Evd.evar_source with
+      | _, (Evar_kinds.VarInstance _ | Evar_kinds.GoalEvar) as x -> x
+      | loc,_ -> loc,Evar_kinds.GoalEvar }
     in
     let info = Typeclasses.mark_unresolvable info in
     Evd.add evd content info
-- 
cgit v1.2.3