Amélioration des messages d'erreurs concernant l'inférence des implicites

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

13 files changed, 111 insertions, 63 deletions

diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index ab8eab6c9e..e6f6891f73 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -134,14 +134,14 @@ let tuple_ref dep n =
 
 (* Binders. *)
 
-let trad_binder avoid nenv = function
-  | CC_untyped_binder -> RHole None
+let trad_binder avoid nenv id = function
+  | CC_untyped_binder -> RHole (dummy_loc,AbstractionType (Name id))
   | CC_typed_binder ty -> Detyping.detype (Global.env()) avoid nenv ty
 
 let rec push_vars avoid nenv = function
   | [] -> ([],avoid,nenv)
   | (id,b) :: bl -> 
-      let b' = trad_binder avoid nenv b in
+      let b' = trad_binder avoid nenv id b in
       let bl',avoid',nenv' = 
 	push_vars (id :: avoid) (add_name (Name id) nenv) bl 
       in
@@ -200,7 +200,9 @@ let rawconstr_of_prog p =
     | CC_tuple (false,_,[e1;e2]) ->
 	let c1 = trad avoid nenv e1 
 	and c2 = trad avoid nenv e2 in
-	RApp (dummy_loc, RRef (dummy_loc,pair), [RHole None;RHole None;c1;c2])
+	RApp (dummy_loc, RRef (dummy_loc,pair),
+	      [RHole (dummy_loc,ImplicitArg (pair,1));
+	       RHole (dummy_loc,ImplicitArg (pair,2));c1;c2])
 
     | CC_tuple (dep,tyl,l) ->
       	let n = List.length l in
@@ -220,7 +222,7 @@ let rawconstr_of_prog p =
 	Detyping.detype (Global.env()) avoid nenv c
 
     | CC_hole c -> 
-	RCast (dummy_loc, RHole None,
+	RCast (dummy_loc, RHole (dummy_loc, QuestionMark),
                Detyping.detype (Global.env()) avoid nenv c)
 
   in
diff --git a/lib/util.ml b/lib/util.ml
index 6632beaf29..cd575bf08a 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -523,6 +523,10 @@ let pr_coma () = str "," ++ spc ()
 let pr_semicolon () = str ";" ++ spc ()
 let pr_bar () = str "|" ++ spc ()
 
+let pr_ord n =
+  let suff = match n mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
+  int n ++ str suff
+
 let rec prlist elem l = match l with 
   | []   -> mt ()
   | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
diff --git a/lib/util.mli b/lib/util.mli
index aa7042903d..6bbe609cbd 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -172,6 +172,7 @@ val pr_str : string -> std_ppcmds
 val pr_coma : unit -> std_ppcmds
 val pr_semicolon : unit -> std_ppcmds
 val pr_bar : unit -> std_ppcmds
+val pr_ord : int -> std_ppcmds
 
 val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index c8aa762449..ca911ad4a1 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -387,6 +387,15 @@ let check_capture loc s ty = function
   | Slam _ when occur_var_ast s ty -> error_capture_loc loc s
   | _ -> ()
 
+let locate_if_isevar loc id = function
+  | RHole _ -> RHole (loc, AbstractionType id)
+  | x -> x
+
+let set_hole_implicit i = function
+  | RRef (loc,r) -> (loc,ImplicitArg (r,i))
+  | RVar (loc,id) -> (loc,ImplicitArg (VarRef id,i))
+  | _ -> anomaly "Only refs have implicits"
+
 let ast_to_rawconstr sigma env allow_soapp lvar =
   let rec dbrec (ids,impls as env) = function
     | Nvar(loc,s) ->
@@ -420,14 +429,14 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	let arityl = Array.of_list (List.map (dbrec env) lA) in
 	RRec (loc,RCoFix n, Array.of_list lf, arityl, defl)
 	  
-    | Node(loc,("PROD"|"LAMBDA"|"LETIN" as k), [c1;Slam(_,ona,c2)]) ->
+    | Node(loc,("PROD"|"LAMBDA"|"LETIN" as k), [c1;Slam(locna,ona,c2)]) ->
 	let na,ids' = match ona with
 	  | Some id -> Name id, Idset.add id ids
 	  | _ -> Anonymous, ids in
 	let c1' = dbrec env c1 and c2' = dbrec (ids',impls) c2 in
 	(match k with
 	   | "PROD" -> RProd (loc, na, c1', c2')
-	   | "LAMBDA" -> RLambda (loc, na, c1', c2')
+	   | "LAMBDA" -> RLambda (loc, na, locate_if_isevar locna na c1', c2')
 	   | "LETIN" -> RLetIn (loc, na, c1', c2')
 	   | _ -> assert false)
 
@@ -448,7 +457,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 		ast_to_global loc (key,l)
 	    | _ -> (dbrec env f, [])
         in
-	  RApp (loc, c, ast_to_impargs env impargs args)
+	  RApp (loc, c, ast_to_impargs c env impargs args)
 
     | Node(loc,"CASES", p:: Node(_,"TOMATCH",tms):: eqns) ->
 	let po = match p with 
@@ -468,7 +477,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	ROldCase (loc,isrec,po,dbrec env c,
 		  Array.of_list (List.map (dbrec env) cl))
 
-    | Node(loc,"ISEVAR",[]) -> RHole (Some loc)
+    | Node(loc,"ISEVAR",[]) -> RHole (loc, QuestionMark)
     | Node(loc,"META",[Num(_,n)]) ->
 	if n<0 then error_metavar_loc loc else RMeta (loc, n)
 
@@ -530,18 +539,19 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	let r = iterated_binder oper (n+1) ty (ids',impls) body in
 	(match oper with
 	   | "PRODLIST" -> RProd(loc, na, dbrec env ty, r)
-	   | "LAMBDALIST" -> RLambda(loc, na, dbrec env ty, r)
+	   | "LAMBDALIST" ->
+	       RLambda(loc, na, locate_if_isevar loc na (dbrec env ty), r)
 	   | _ -> assert false)
     | body -> dbrec env body
 
-  and ast_to_impargs env l args =
+  and ast_to_impargs c env l args =
     let rec aux n l args = match (l,args) with 
       | (i::l',Node(loc, "EXPL", [Num(_,j);a])::args') ->
 	  if i=n & j>=i then
 	    if j=i then 
 	      (dbrec env a)::(aux (n+1) l' args')
 	    else 
-	      (RHole None)::(aux (n+1) l' args)
+	      (RHole (set_hole_implicit i c))::(aux (n+1) l' args)
 	  else 
 	    if i<>n then
 	      error ("Bad explicitation number: found "^
@@ -551,7 +561,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 		   (string_of_int j)^" but was expecting "^(string_of_int i))
       | (i::l',a::args') -> 
 	  if i=n then 
-	    (RHole None)::(aux (n+1) l' args)
+	    (RHole (set_hole_implicit i c))::(aux (n+1) l' args)
 	  else 
 	    (dbrec env a)::(aux (n+1) l args')
       | ([],args) -> ast_to_args env args
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 407bec37fc..717d509e86 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -131,8 +131,8 @@ let parse_string f x =
 
 let slam_ast (_,fin) id ast =
   match id with
-    | Coqast.Nvar ((deb,_), s) -> Coqast.Slam ((deb,fin), Some s, ast)
-    | Coqast.Nmeta ((deb,_), s) -> Coqast.Smetalam ((deb,fin), s, ast)
+    | Coqast.Nvar (loc, s) -> Coqast.Slam (loc, Some s, ast)
+    | Coqast.Nmeta (loc, s) -> Coqast.Smetalam (loc, s, ast)
     | _ -> invalid_arg "Ast.slam_ast"
 
 (* This is to interpret the macro $ABSTRACT used in binders        *)
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index ca13c1c16e..aef3fb9c37 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -63,12 +63,12 @@ let error_needs_inversion env x t =
 (* A) Typing old cases                                               *)
 (* This was previously in Indrec but creates existential holes       *)
 
-let mkExistential isevars env = new_isevar isevars env (new_Type ())
+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 in 
+    | [] -> mkExistential isevars env (dummy_loc, QuestionMark) in 
   crec env (List.rev cstr.cs_args)
 
 let rec_branch_scheme env isevars (sp,j) recargs cstr =
@@ -78,7 +78,8 @@ 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 in
+		  let t = mkExistential isevars env (dummy_loc, QuestionMark)
+		  in
 		  mkArrow t
 		    (crec (push_rel (Anonymous,None,t) env)
 		       (List.rev (lift_rel_context 1 (List.rev rea)),reca))
@@ -87,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
+      | [],[] -> mkExistential isevars env (dummy_loc, QuestionMark)
       | _ -> anomaly "rec_branch_scheme"
   in 
   crec env (List.rev cstr.cs_args,recargs) 
@@ -427,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 ty)::evl))
+	    (new_isevar isevars env (dummy_loc, QuestionMark) ty)::evl))
       ntys (env,[]) in
   let expected_typ = applist (mkInd tyi,evarl) in
      (* devrait être indifférent d'exiger leq ou pas puisque pour 
@@ -962,7 +963,7 @@ let infer_predicate loc env isevars typs cstrs indf =
 	(* Heuristic to avoid comparison between non-variables algebric univs*)
 	new_Type ()
       else
-	mkExistential isevars env
+	mkExistential isevars env (loc, CasesType)
     in
     if array_for_all (fun (_,_,typ) -> the_conv_x_leq env isevars typ mtyp) eqns
     then
@@ -1499,7 +1500,7 @@ let extract_predicate_conclusion nargs pred =
       | _ -> (* eta-expansion *) applist (lift 1 p, [mkRel 1]) in
   iterate decomp_lam_force nargs pred
 
-let prepare_predicate_from_tycon dep env isevars tomatchs c =
+let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
   let cook (n, l, env) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
 	let indf' = lift_inductive_family n indf in
@@ -1519,7 +1520,7 @@ let prepare_predicate_from_tycon dep env isevars tomatchs c =
  (* let c = whd_betadeltaiota env (evars_of isevars) c in *)
     (* We turn all subterms possibly dependent into an evar with maximum ctxt*)
     if isEvar c or List.exists (eq_constr c) allargs then
-      mkExistential isevars env
+      mkExistential isevars env (loc, CasesType)
     else
       map_constr_with_full_binders push_rel build_skeleton env c in
   build_skeleton env (lift n c)
@@ -1559,12 +1560,12 @@ let build_initial_predicate env sigma isdep pred tomatchl =
  *        else error! (can not treat mixed dependent and non dependent case
  *)
 
-let prepare_predicate typing_fun isevars env tomatchs tycon = function
+let prepare_predicate loc typing_fun isevars env tomatchs tycon = function
   | None ->
       (match tycon with
        | None -> None
        | Some t ->
-	 let pred = prepare_predicate_from_tycon false env isevars tomatchs t in
+	 let pred = prepare_predicate_from_tycon loc false env isevars tomatchs t in
 	 Some
 	  (build_initial_predicate env (evars_of isevars) false pred tomatchs))
   | Some pred ->
@@ -1613,7 +1614,7 @@ let compile_cases loc (typing_fun,isevars) tycon env (predopt, tomatchl, eqns)=
 
   (* We build the elimination predicate if any and check its consistency *)
   (* with the type of arguments to match *)
-  let pred = prepare_predicate typing_fun isevars env tomatchs tycon predopt in
+  let pred = prepare_predicate loc typing_fun isevars env tomatchs tycon predopt in
 
   (* We deal with initial aliases *)
   let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e9a1b03bac..090d6e1d1c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -325,7 +325,9 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) = 
   let ks =
     List.fold_left
-      (fun ks b -> (new_isevar isevars env (substl ks b)) :: ks)
+      (fun ks b ->
+	 let dloc = (Rawterm.dummy_loc,Rawterm.QuestionMark) in
+	 (new_isevar isevars env dloc (substl ks b)) :: ks)
       [] bs
   in
   if (list_for_all2eq 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c556f998eb..726d3b7470 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -221,12 +221,14 @@ let do_restrict_hyps sigma ev args =
 type evar_constraint = conv_pb * constr * constr
 type evar_defs =
     { mutable evars : Evd.evar_map;
-      mutable conv_pbs : evar_constraint list }
+      mutable conv_pbs : evar_constraint list;
+      mutable history : (int * (loc * Rawterm.hole_kind)) list }
 
-let create_evar_defs evd = { evars=evd; conv_pbs=[] }
+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
 
 (* 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
@@ -339,12 +341,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 typ =
+let new_isevar isevars env loc 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;
   evar
 
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 7519f51cdc..f75bd31b1f 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -10,6 +10,7 @@
 
 (*i*)
 open Names
+open Rawterm
 open Term
 open Sign
 open Evd
@@ -46,6 +47,7 @@ type evar_defs
 val evars_of :  evar_defs ->  evar_map
 val create_evar_defs :  evar_map ->  evar_defs
 val evars_reset_evd :  evar_map ->  evar_defs -> unit
+val evar_source : existential_key -> evar_defs -> loc * hole_kind
 
 type evar_constraint = conv_pb * constr * constr
 val add_conv_pb :  evar_defs -> evar_constraint -> unit
@@ -55,7 +57,7 @@ val ise_try :  evar_defs -> (unit -> bool) list -> bool
 val ise_undefined :  evar_defs -> constr -> bool
 val has_undefined_isevars :  evar_defs -> constr -> bool
 
-val new_isevar :  evar_defs -> env -> constr -> constr
+val new_isevar :  evar_defs -> env -> loc * hole_kind -> constr -> constr
 
 val is_eliminator : constr -> bool
 val head_is_embedded_evar :  evar_defs -> constr -> bool
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a18b5499c5..58aa52d164 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -132,6 +132,21 @@ let evar_type_fixpoint loc env isevars lna lar vdefj =
             i lna vdefj lar
       done
 
+let error_unsolvable_implicit (loc,kind) =
+  let message = match kind with
+    | QuestionMark -> str "Cannot infer a term for this placeholder"
+    | CasesType ->
+	str "Cannot infer the type of this pattern-matching problem"
+    | AbstractionType (Name id) ->
+	str "Cannot infer a type for " ++ Nameops.pr_id id
+    | AbstractionType Anonymous ->
+	str "Cannot infer a type of this anonymous abstraction"
+    | ImplicitArg (c,n) ->
+	str "Cannot infer the " ++ pr_ord n ++
+	str " implicit argument of " ++ Nametab.pr_global_env (Global.env()) c
+  in
+    user_err_loc (loc,"pretype",message)
+
 let check_branches_message loc env isevars c (explft,lft) = 
   for i = 0 to Array.length explft - 1 do
     if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then 
@@ -213,14 +228,9 @@ let rec pretype tycon env isevars lvar lmeta = function
   | RHole loc ->
       if !compter then nbimpl:=!nbimpl+1;
       (match tycon with
-	 | Some ty -> { uj_val = new_isevar isevars env ty; uj_type = ty }
-	 | None ->
-	     (match loc with
-		  None -> error "There is an implicit argument I cannot solve"
-		| Some loc -> 
-		    user_err_loc
-		      (loc,"pretype",
-		       (str "Cannot infer a term for this placeholder"))))
+	 | Some ty ->
+	     { uj_val = new_isevar isevars env loc ty; uj_type = ty }
+	 | None -> error_unsolvable_implicit loc)
 
   | RRec (loc,fixkind,names,lar,vdef) ->
       let larj =
@@ -323,7 +333,8 @@ let rec pretype tycon env isevars lvar lmeta = function
       let (IndType (indf,realargs) as indt) = 
 	try find_rectype env (evars_of isevars) cj.uj_type
 	with Not_found ->
-          error_case_not_inductive_loc loc env (evars_of isevars) cj in
+	  let cloc = loc_of_rawconstr c in
+	  error_case_not_inductive_loc cloc env (evars_of isevars) cj in
       let (dep,pj) = match po with
 	| Some p ->
             let pj = pretype empty_tycon env isevars lvar lmeta p in
@@ -441,7 +452,8 @@ and pretype_type valcon env isevars lvar lmeta = function
 	       utj_type = Retyping.get_sort_of env (evars_of isevars) v }
 	 | None ->
 	     let s = new_Type_sort () in
-	     { utj_val = new_isevar isevars env (mkSort s); utj_type = s})
+	     { utj_val = new_isevar isevars env loc (mkSort s);
+	       utj_type = s})
   | c ->
       let j = pretype empty_tycon env isevars lvar lmeta c in
       let tj = inh_coerce_to_sort env isevars j in
@@ -471,15 +483,15 @@ let unsafe_infer_type valcon isevars env lvar lmeta constr =
  *)
 (* assumes the defined existentials have been replaced in c (should be
    done in unsafe_infer and unsafe_infer_type) *)
-let check_evars fail_evar initial_sigma sigma c =
+let check_evars fail_evar initial_sigma isevars c =
+  let sigma = evars_of isevars in
   let rec proc_rec c =
     match kind_of_term c with
       | Evar (ev,args as k) ->
           assert (Evd.in_dom sigma ev);
 	  if not (Evd.in_dom initial_sigma ev) then
 	    (if fail_evar then
-	      errorlabstrm "whd_ise"
-		(str"There is an unknown subterm I cannot solve"))
+	       error_unsolvable_implicit (evar_source ev isevars))
       | _ -> iter_constr proc_rec c      
   in
   proc_rec c
@@ -495,9 +507,8 @@ type open_constr = evar_map * constr
 let ise_resolve_casted_gen fail_evar sigma env lvar lmeta typ c =
   let isevars = create_evar_defs sigma in
   let j = unsafe_infer (mk_tycon typ) isevars env lvar lmeta c in
-  let new_sigma = evars_of isevars in
-  check_evars fail_evar sigma new_sigma (mkCast(j.uj_val,j.uj_type));
-  (new_sigma, j)
+  check_evars fail_evar sigma isevars (mkCast(j.uj_val,j.uj_type));
+  (evars_of isevars, j)
 
 let ise_resolve_casted sigma env typ c =
   ise_resolve_casted_gen true sigma env [] [] typ c
@@ -509,16 +520,14 @@ let ise_infer_gen fail_evar sigma env lvar lmeta exptyp c =
   let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in
   let isevars = create_evar_defs sigma in
   let j = unsafe_infer tycon isevars env lvar lmeta c in
-  let new_sigma = evars_of isevars in
-  check_evars fail_evar sigma new_sigma (mkCast(j.uj_val,j.uj_type));
-  (new_sigma, j)
+  check_evars fail_evar sigma isevars (mkCast(j.uj_val,j.uj_type));
+  (evars_of isevars, j)
 
 let ise_infer_type_gen fail_evar sigma env lvar lmeta c =
   let isevars = create_evar_defs sigma in
   let tj = unsafe_infer_type empty_valcon isevars env lvar lmeta c in
-  let new_sigma = evars_of isevars in
-  check_evars fail_evar sigma new_sigma tj.utj_val;
-  (new_sigma, tj)
+  check_evars fail_evar sigma isevars tj.utj_val;
+  (evars_of isevars, tj)
 
 type meta_map = (int * unsafe_judgment) list
 type var_map = (identifier * unsafe_judgment) list
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index d82d7fbc81..1237a9560a 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -32,6 +32,12 @@ type fix_kind = RFix of (int array * int) | RCoFix of int
 
 type binder_kind = BProd | BLambda | BLetIn
 
+type hole_kind =
+  | ImplicitArg of global_reference * int
+  | AbstractionType of name
+  | QuestionMark
+  | CasesType
+
 type 'ctxt reference =
   | RConst of constant * 'ctxt
   | RInd of inductive * 'ctxt
@@ -56,7 +62,7 @@ type rawconstr =
   | RRec of loc * fix_kind * identifier array * 
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
-  | RHole of loc option
+  | RHole of (loc * hole_kind)
   | RCast of loc * rawconstr * rawconstr
   | RDynamic of loc * Dyn.t
 
@@ -69,7 +75,6 @@ type rawconstr =
    dans le contexte servant à typer les body ???]
 
    - boolean in POldCase means it is recursive
-   - option in PHole tell if the "?" was apparent or has been implicitely added
 i*)
 
 let dummy_loc = (0,0)
@@ -87,8 +92,7 @@ let loc_of_rawconstr = function
   | ROldCase (loc,_,_,_,_) -> loc
   | RRec (loc,_,_,_,_) -> loc
   | RSort (loc,_) -> loc
-  | RHole (Some loc) -> loc
-  | RHole (None) -> dummy_loc
+  | RHole (loc,_) -> loc
   | RCast (loc,_,_) -> loc
   | RDynamic (loc,_) -> loc
 
@@ -105,7 +109,7 @@ let set_loc_of_rawconstr loc = function
   | ROldCase (_,a,b,c,d) -> ROldCase (loc,a,b,c,d) 
   | RRec (_,a,b,c,d) -> RRec (loc,a,b,c,d) 
   | RSort (_,a)      -> RSort (loc,a) 
-  | RHole _          -> RHole (Some loc)
+  | RHole (_,a)      -> RHole (loc,a)
   | RCast (_,a,b)    -> RCast (loc,a,b) 
   | RDynamic (_,d)   -> RDynamic (loc,d)
 
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 8d5184299f..ad7fadf5d8 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -31,6 +31,12 @@ type fix_kind = RFix of (int array * int) | RCoFix of int
 
 type binder_kind = BProd | BLambda | BLetIn
 
+type hole_kind =
+  | ImplicitArg of global_reference * int
+  | AbstractionType of name
+  | QuestionMark
+  | CasesType
+
 type 'ctxt reference =
   | RConst of constant * 'ctxt
   | RInd of inductive * 'ctxt
@@ -54,7 +60,7 @@ type rawconstr =
   | RRec of loc * fix_kind * identifier array * 
       rawconstr array * rawconstr array
   | RSort of loc * rawsort
-  | RHole of loc option
+  | RHole of (loc * hole_kind)
   | RCast of loc * rawconstr * rawconstr
   | RDynamic of loc * Dyn.t
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 2d93c6fd35..4041d311c5 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -95,10 +95,14 @@ let explain_elim_arity ctx ind aritylst c pj okinds =
 let explain_case_not_inductive ctx cj =
   let pc = prterm_env ctx cj.uj_val in
   let pct = prterm_env ctx cj.uj_type in
-  str "In Cases expression, the matched term" ++ brk(1,1) ++ pc ++ spc () ++ 
-  str "has type" ++ brk(1,1) ++ pct ++ spc () ++ 
-  str "which is not a (co-)inductive type"
-  
+    match kind_of_term cj.uj_type with
+      | Evar _ -> 
+	  str "Cannot infer a type for this expression"
+      | _ ->
+	  str "This term" ++ brk(1,1) ++ pc ++ spc () ++ 
+	  str "has type" ++ brk(1,1) ++ pct ++ spc () ++ 
+	  str "which is not a (co-)inductive type"
+
 let explain_number_branches ctx cj expn =
   let pc = prterm_env ctx cj.uj_val in
   let pct = prterm_env ctx cj.uj_type in