From 32e2b1ba856f330dae03fbbf16365a08c2cc2f20 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 21 Aug 2014 12:39:32 +0200
Subject: Fix source of initial goal.

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

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 98be5a5d5b..661b32601c 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -39,7 +39,8 @@ let init sigma =
   | [] ->  [], { solution = sigma; comb = []; }
   | (env, typ) :: l ->
     let ret, { solution = sol; comb = comb } = aux l in
-    let (new_defs , econstr) = Evarutil.new_evar sol env typ in
+    let src = (Loc.ghost,Evar_kinds.GoalEvar) in
+    let (new_defs , econstr) = Evarutil.new_evar sol env ~src typ in
     let (e, _) = Term.destEvar econstr in
     let gl = Goal.build e in
     let entry = (econstr, typ) :: ret in
-- 
cgit v1.2.3