From 14ba28e2b4ff3e93e629e4fe0842d74dd30557b3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 22 Dec 2009 16:47:10 +0000
Subject: Attached evar source to the evar_info and add location to
 tclWITHHOLES errors

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12605 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/proof_trees.ml |  3 ++-
 proofs/refiner.ml     | 12 +++++++-----
 2 files changed, 9 insertions(+), 6 deletions(-)

(limited to 'proofs')

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 8c808e1c84..a5bd073a30 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -36,7 +36,8 @@ let is_bind = function
 let mk_goal hyps cl extra =
   { evar_hyps = hyps; evar_concl = cl;
     evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
-    evar_body = Evar_empty; evar_extra = extra }
+    evar_body = Evar_empty; evar_source = (dummy_loc,GoalEvar); 
+    evar_extra = extra }
 
 (* Functions on proof trees *)
 
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index be584790b6..a320b67cda 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -943,7 +943,7 @@ let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } =
 
 (* Check that holes in arguments have been resolved *)
 
-let check_evars sigma evm gl =
+let check_evars env sigma evm gl =
   let origsigma = gl.sigma in
   let rest =
     Evd.fold (fun ev evi acc ->
@@ -952,13 +952,15 @@ let check_evars sigma evm gl =
       evm Evd.empty
   in
   if rest <> Evd.empty then
-    errorlabstrm "apply" (str"Uninstantiated existential "++
-      str(plural (List.length (Evd.to_list rest)) "variable")++str": " ++
-      fnl () ++ pr_evar_map rest);;
+    let (evk,evi) = List.hd (Evd.to_list rest) in
+    let (loc,k) = evar_source evk rest in
+    let evi = Evarutil.nf_evar_info sigma evi in
+    Pretype_errors.error_unsolvable_implicit loc env sigma evi k None
 
 let tclWITHHOLES accept_unresolved_holes tac sigma c gl =
   if sigma == project gl then tac c gl
   else
     let res = tclTHEN (tclEVARS sigma) (tac c) gl in
-    if not accept_unresolved_holes then check_evars (fst res).sigma sigma gl;
+    if not accept_unresolved_holes then
+      check_evars (pf_env gl) (fst res).sigma sigma gl;
     res
-- 
cgit v1.2.3