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

4 files changed, 49 insertions, 45 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 9035bb54db..0d9a51ba37 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -19,6 +19,20 @@ open Environ
 open Libnames
 open Mod_subst
 
+(* The kinds of existential variable *)
+
+type obligation_definition_status = Define of bool | Expand
+
+type hole_kind =
+  | ImplicitArg of global_reference * (int * identifier option) * bool
+  | BinderType of name
+  | QuestionMark of obligation_definition_status
+  | CasesType
+  | InternalHole
+  | TomatchTypeParameter of inductive * int
+  | GoalEvar
+  | ImpossibleCase
+
 (* The type of mappings for existential variables *)
 
 type evar = existential_key
@@ -35,6 +49,7 @@ type evar_info = {
   evar_hyps : named_context_val;
   evar_body : evar_body;
   evar_filter : bool list;
+  evar_source : hole_kind located;
   evar_extra : Dyn.t option}
 
 let make_evar hyps ccl = {
@@ -42,6 +57,7 @@ let make_evar hyps ccl = {
   evar_hyps = hyps;
   evar_body = Evar_empty;
   evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
+  evar_source = (dummy_loc,InternalHole);
   evar_extra = None
 }
 
@@ -407,25 +423,12 @@ let metamap_to_list m =
 (*************************)
 (* Unification state *)
 
-type obligation_definition_status = Define of bool | Expand
-
-type hole_kind =
-  | ImplicitArg of global_reference * (int * identifier option) * bool
-  | BinderType of name
-  | QuestionMark of obligation_definition_status
-  | CasesType
-  | InternalHole
-  | TomatchTypeParameter of inductive * int
-  | GoalEvar
-  | ImpossibleCase
-
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * Environ.env * constr * constr
 type evar_map =
     { evars : EvarMap.t;
       conv_pbs : evar_constraint list;
       last_mods : ExistentialSet.t;
-      history : (existential_key * (loc * hole_kind)) list;
       metas : clbinding Metamap.t }
 
 (*** Lifting primitive from EvarMap. ***)
@@ -441,7 +444,6 @@ let merge d1 d2 = {
   evars = EvarMap.merge d1.evars d2.evars ;
   conv_pbs = List.rev_append d1.conv_pbs d2.conv_pbs ;
   last_mods = ExistentialSet.union d1.last_mods d2.last_mods ;
-  history = List.rev_append d1.history d2.history ;
   metas = Metamap.fold (fun k m r -> Metamap.add k m r) d2.metas d1.metas
 }
 let add d e i = { d with evars=EvarMap.add d.evars e i }
@@ -492,7 +494,7 @@ let subst_evar_map = subst_evar_defs_light
 
 (* spiwack: deprecated *)
 let create_evar_defs sigma = { sigma with
-  conv_pbs=[]; last_mods=ExistentialSet.empty; history=[]; metas=Metamap.empty }
+  conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty }
 (* spiwack: tentatively deprecated *)
 let create_goal_evar_defs sigma = { sigma with
    conv_pbs=[]; last_mods=ExistentialSet.empty; metas=Metamap.empty }
@@ -500,15 +502,12 @@ let empty =  {
   evars=EvarMap.empty;
   conv_pbs=[];
   last_mods = ExistentialSet.empty;
-  history=[];
   metas=Metamap.empty
 }
 
 let evars_reset_evd evd d = {d with evars = evd.evars}
 let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs}
-let evar_source evk d =
-  try List.assoc evk d.history
-  with Not_found -> (dummy_loc, InternalHole)
+let evar_source evk d = (EvarMap.find d.evars evk).evar_source
 
 (* define the existential of section path sp as the constr body *)
 let define evk body evd =
@@ -534,8 +533,8 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd =
        evar_concl = ty;
        evar_body = Evar_empty;
        evar_filter = filter;
-       evar_extra = None};
-    history = (evk,src)::evd.history }
+       evar_source = src;
+       evar_extra = None} }
 
 let is_defined_evar evd (evk,_) = EvarMap.is_defined evd.evars evk
 
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index fed11f1ffa..3974e65b42 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -77,6 +77,25 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding
 
 
 (*********************************************************************)
+(*** Kinds of existential variables ***)
+
+(* Should the obligation be defined (opaque or transparent (default)) or
+   defined transparent and expanded in the term? *)
+
+type obligation_definition_status = Define of bool | Expand
+
+(* Evars *)
+type hole_kind =
+  | ImplicitArg of global_reference * (int * identifier option) * bool (* Force inference *)
+  | BinderType of name
+  | QuestionMark of obligation_definition_status
+  | CasesType
+  | InternalHole
+  | TomatchTypeParameter of inductive * int
+  | GoalEvar
+  | ImpossibleCase
+
+(*********************************************************************)
 (*** Existential variables and unification states ***)
 
 (* A unification state (of type [evar_map]) is primarily a finite mapping
@@ -102,6 +121,7 @@ type evar_info = {
   evar_hyps : named_context_val;
   evar_body : evar_body;
   evar_filter : bool list;
+  evar_source : hole_kind located;
   evar_extra : Dyn.t option}
 
 val eq_evar_info : evar_info -> evar_info -> bool
@@ -160,24 +180,6 @@ val subst_evar_defs_light : substitution -> evar_map -> evar_map
 val evars_reset_evd  : evar_map ->  evar_map -> evar_map
 
 
-
-
-(* Should the obligation be defined (opaque or transparent (default)) or
-   defined transparent and expanded in the term? *)
-
-type obligation_definition_status = Define of bool | Expand
-
-(* Evars *)
-type hole_kind =
-  | ImplicitArg of global_reference * (int * identifier option) * bool (* Force inference *)
-  | BinderType of name
-  | QuestionMark of obligation_definition_status
-  | CasesType
-  | InternalHole
-  | TomatchTypeParameter of inductive * int
-  | GoalEvar
-  | ImpossibleCase
-
 (* spiwack: [is_undefined_evar] should be considered a candidate
                    for moving to evarutils *)
 val is_undefined_evar :  evar_map -> constr -> bool
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