From 502e61ec1ac488dd430ce6654c7a6947c6f7d1c3 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Apr 2014 18:12:00 +0200
Subject: Evars introduced by Proofview refining are flagged as GoalEvar. For
 some reasons, some code depends on it.

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

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 0600a9c8ba..c7ffca3eb2 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -860,7 +860,8 @@ struct
   type handle = Evd.evar_map * goal list
 
   let new_evar (evd, evs) env typ =
-    let (evd, ev) = Evarutil.new_evar evd env typ in
+    let src = (Loc.ghost, Evar_kinds.GoalEvar) in
+    let (evd, ev) = Evarutil.new_evar evd env ~src typ in
     let (evk, _) = Term.destEvar ev in
     let h = (evd, build_goal evk :: evs) in
     (h, ev)
-- 
cgit v1.2.3