Deuxième passe sur la localisation des messages d'erreurs sur les evars non définies

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2633 85f007b7-540e-0410-9357-904b9bb8a0f7

8 files changed, 44 insertions, 29 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index aef3fb9c37..d1d401bc75 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -68,7 +68,7 @@ let mkExistential isevars env loc = new_isevar isevars env loc (new_Type ())
 let norec_branch_scheme env isevars cstr =
   let rec crec env = function
     | d::rea -> mkProd_or_LetIn d (crec (push_rel d env) rea)
-    | [] -> mkExistential isevars env (dummy_loc, QuestionMark) in 
+    | [] -> mkExistential isevars env (dummy_loc, InternalHole) in 
   crec env (List.rev cstr.cs_args)
 
 let rec_branch_scheme env isevars (sp,j) recargs cstr =
@@ -78,7 +78,7 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr =
 	  let d =
  	    match dest_recarg ra with 
 	      | Mrec k when k=j ->
-		  let t = mkExistential isevars env (dummy_loc, QuestionMark)
+		  let t = mkExistential isevars env (dummy_loc, InternalHole)
 		  in
 		  mkArrow t
 		    (crec (push_rel (Anonymous,None,t) env)
@@ -88,7 +88,7 @@ let rec_branch_scheme env isevars (sp,j) recargs cstr =
 
       | (name,Some b,c as d)::rea, reca -> 
 	  mkLetIn (name,b,body_of_type c,crec (push_rel d env) (rea,reca))
-      | [],[] -> mkExistential isevars env (dummy_loc, QuestionMark)
+      | [],[] -> mkExistential isevars env (dummy_loc, InternalHole)
       | _ -> anomaly "rec_branch_scheme"
   in 
   crec env (List.rev cstr.cs_args,recargs) 
@@ -428,7 +428,7 @@ let inh_coerce_to_ind isevars env ty tyi =
     List.fold_right
       (fun (na,ty) (env,evl) ->
 	 (push_rel (na,None,ty) env,
-	    (new_isevar isevars env (dummy_loc, QuestionMark) ty)::evl))
+	    (new_isevar isevars env (dummy_loc, InternalHole) ty)::evl))
       ntys (env,[]) in
   let expected_typ = applist (mkInd tyi,evarl) in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5c6b2c6b79..46f9568fa5 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -83,8 +83,7 @@ let inh_app_fun env isevars j =
   match kind_of_term t with
     | Prod (_,_,_) -> j
     | Evar ev when not (is_defined_evar isevars ev) ->
-	let (sigma',t) = define_evar_as_arrow (evars_of isevars) ev in
-	evars_reset_evd sigma' isevars;
+	let t = define_evar_as_arrow isevars ev in
 	{ uj_val = j.uj_val; uj_type = t }
     | _ ->
        	(try
@@ -106,8 +105,7 @@ let inh_coerce_to_sort env isevars j =
   match kind_of_term typ with
     | Sort s -> { utj_val = j.uj_val; utj_type = s }
     | Evar ev when not (is_defined_evar isevars ev) ->
-	let (sigma', s) = define_evar_as_sort (evars_of isevars) ev in
-	evars_reset_evd sigma' isevars;
+	let s = define_evar_as_sort isevars ev in
 	{ utj_val = j.uj_val; utj_type = s }
     | _ ->
         let j1 = inh_tosort_force env isevars j in 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 090d6e1d1c..049659b895 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -326,7 +326,7 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
   let ks =
     List.fold_left
       (fun ks b ->
-	 let dloc = (Rawterm.dummy_loc,Rawterm.QuestionMark) in
+	 let dloc = (Rawterm.dummy_loc,Rawterm.InternalHole) in
 	 (new_isevar isevars env dloc (substl ks b)) :: ks)
       [] bs
   in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 726d3b7470..6a1fb9edec 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -151,8 +151,7 @@ let refresh_universes t =
    cumulativity now includes Prop and Set in Type. *)
 let new_type_var env sigma =
   let instance = make_evar_instance env in
-  let (sigma',c) = new_isevar_sign env sigma (new_Type ()) instance in
-  (sigma', c)
+  new_isevar_sign env sigma (new_Type ()) instance
 
 let split_evar_to_arrow sigma (ev,args) =
   let evd = Evd.map sigma ev in
@@ -169,16 +168,7 @@ let split_evar_to_arrow sigma (ev,args) =
   let evrng =
     fst (destEvar rng), array_cons (mkRel 1) (Array.map (lift 1) args) in
   let prod' = mkProd (x, mkEvar evdom, mkEvar evrng) in
-  (sigma3, prod', evdom, evrng)
-
-let define_evar_as_arrow sigma ev =
-  let (sigma, prod, _, _) = split_evar_to_arrow sigma ev in
-  (sigma, prod)
-
-let define_evar_as_sort sigma (ev,args) =
-  let s = new_Type () in
-  let sigma = Evd.define sigma ev s in
-  (sigma, destSort s)
+  (sigma3,prod', evdom, evrng)
 
 (* Redefines an evar with a smaller context (i.e. it may depend on less
  * variables) such that c becomes closed.
@@ -228,7 +218,9 @@ let create_evar_defs evd = { evars=evd; conv_pbs=[]; history=[] }
 let evars_of d = d.evars
 let evars_reset_evd evd d = d.evars <- evd
 let add_conv_pb d pb = d.conv_pbs <- pb::d.conv_pbs
-let evar_source ev d = List.assoc ev d.history
+let evar_source ev d =
+  try List.assoc ev d.history
+  with Failure _ -> (Rawterm.dummy_loc, Rawterm.InternalHole)
 
 (* ise_try [f1;...;fn] tries fi() for i=1..n, restoring the evar constraints
  * when fi returns false or an exception. Returns true if one of the fi
@@ -290,7 +282,8 @@ let real_clean isevars ev args rhs =
 	    else begin
 	      let (sigma,rc) = do_restrict_hyps isevars.evars ev args' in
 	      isevars.evars <- sigma;
-
+              isevars.history <- 
+                (fst (destEvar rc),evar_source ev isevars)::isevars.history;
 	      rc
 	    end
 	  else
@@ -341,13 +334,13 @@ let push_rel_context_to_named_context env =
     (rel_context env) ~init:([],ids_of_named_context sign0,sign0)
   in (subst, reset_with_named_context sign env)
 
-let new_isevar isevars env loc typ =
+let new_isevar isevars env src typ =
   let subst,env' = push_rel_context_to_named_context env in
   let typ' = substl subst typ in
   let instance = make_evar_instance_with_rel env in
   let (sigma',evar) = new_isevar_sign env' isevars.evars typ' instance in
   isevars.evars <- sigma';
-  isevars.history <- (fst (destEvar evar),loc)::isevars.history;
+  isevars.history <- (fst (destEvar evar),src)::isevars.history;
   evar
 
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
@@ -487,6 +480,7 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
 	       evar_body = Evar_empty } in
   isevars.evars <-
     Evd.define (Evd.add isevars.evars newev info) ev (mkEvar (newev,nargs));
+  isevars.history <- (newev,evar_source ev isevars)::isevars.history;
   [ev]
 
 
@@ -544,6 +538,26 @@ let empty_valcon = None
 (* Builds a value constraint *)
 let mk_valcon c = Some c
 
+(* Refining an evar to a product or a sort *)
+
+let refine_evar_as_arrow isevars ev =
+  let (sigma,prod,evdom,evrng) = split_evar_to_arrow isevars.evars ev in
+  evars_reset_evd sigma isevars;
+  let hst = evar_source (fst ev) isevars in
+  isevars.history <- (fst evrng,hst)::(fst evdom, hst)::isevars.history;
+  (prod,evdom,evrng)
+
+let define_evar_as_arrow isevars ev =
+  let (prod,_,_) = refine_evar_as_arrow isevars ev in
+  prod
+
+let define_evar_as_sort isevars (ev,args) =
+  let s = new_Type () in
+  let sigma' = Evd.define isevars.evars ev s in
+  evars_reset_evd sigma' isevars;
+  destSort s
+
+
 (* Propagation of constraints through application and abstraction:
    Given a type constraint on a functional term, returns the type
    constraint on its domain and codomain. If the input constraint is
@@ -557,8 +571,7 @@ let split_tycon loc env isevars = function
       match kind_of_term t with
         | Prod (na,dom,rng) -> Some dom, Some rng
 	| Evar (n,_ as ev) when not (Evd.is_defined isevars.evars n) ->
-	    let (sigma',_,evdom,evrng) = split_evar_to_arrow sigma ev in
-	    evars_reset_evd sigma' isevars;
+	    let (_,evdom,evrng) = refine_evar_as_arrow isevars ev in
 	    Some (mkEvar evdom), Some (mkEvar evrng)
 	| _ -> error_not_product_loc loc env sigma c
 
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index f75bd31b1f..4fce79be28 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -65,8 +65,8 @@ val solve_simple_eqn :
   (env ->  evar_defs -> conv_pb -> constr -> constr -> bool)
   -> env ->  evar_defs -> conv_pb * existential * constr -> bool
 
-val define_evar_as_arrow :  evar_map -> existential ->  evar_map * types
-val define_evar_as_sort :  evar_map -> existential ->  evar_map * sorts
+val define_evar_as_arrow : evar_defs -> existential -> types
+val define_evar_as_sort : evar_defs -> existential -> sorts
 
 (* Value/Type constraints *)
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 58aa52d164..66105709c2 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -144,6 +144,8 @@ let error_unsolvable_implicit (loc,kind) =
     | ImplicitArg (c,n) ->
 	str "Cannot infer the " ++ pr_ord n ++
 	str " implicit argument of " ++ Nametab.pr_global_env (Global.env()) c
+    | InternalHole ->
+        str "Cannot infer a term for an internal placeholder"
   in
     user_err_loc (loc,"pretype",message)
 
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 1237a9560a..f69d22dfc8 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -37,6 +37,7 @@ type hole_kind =
   | AbstractionType of name
   | QuestionMark
   | CasesType
+  | InternalHole
 
 type 'ctxt reference =
   | RConst of constant * 'ctxt
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index ad7fadf5d8..973bac7192 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -36,6 +36,7 @@ type hole_kind =
   | AbstractionType of name
   | QuestionMark
   | CasesType
+  | InternalHole
 
 type 'ctxt reference =
   | RConst of constant * 'ctxt