Correction d'un bug dans l'affichage du message d'erreur real_clean

(cas d'un terme sans Rel libre), introduction au passage d'un nouveau
type d'evar EvarGoal pour raffinement du message d'erreur.



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

15 files changed, 38 insertions, 27 deletions

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 514c0811c..0c5e6dbae 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -348,7 +348,7 @@ let rec subst_aconstr subst bound raw =
 	if ref' == ref then raw else
 	  AHole (Evd.InternalHole)
   | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType 
-    | Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
+    | Evd.InternalHole | Evd.TomatchTypeParameter _ | Evd.GoalEvar ) -> raw
 
   | ACast (r1,k) -> 
       match k with
diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 5f4293abf..1c35f9f72 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -132,7 +132,7 @@ let clenv_environments_evars env evd bound t =
 
 let clenv_conv_leq env sigma t c bound =
   let ty = Retyping.get_type_of env sigma c in
-  let evd = Evd.create_evar_defs sigma in
+  let evd = Evd.create_goal_evar_defs sigma in
   let evars,args,_ = clenv_environments_evars env evd (Some bound) ty in
   let evars = Evarconv.the_conv_x_leq env t (applist (c,args)) evars in
   let evars,_ = Evarconv.consider_remaining_unif_problems env evars in
@@ -141,7 +141,7 @@ let clenv_conv_leq env sigma t c bound =
   args
 
 let mk_clenv_from_n gls n (c,cty) =
-  let evd = create_evar_defs gls.sigma in
+  let evd = create_goal_evar_defs gls.sigma in
   let (env,args,concl) = clenv_environments evd n cty in
   { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args));
     templtyp = mk_freelisted concl;
@@ -263,7 +263,8 @@ let clenv_pose_dependent_evars clenv =
   List.fold_left
     (fun clenv mv ->
       let ty = clenv_meta_type clenv mv in
-      let (evd,evar) = new_evar clenv.evd (cl_env clenv) ty in
+      let (evd,evar) = 
+	new_evar clenv.evd (cl_env clenv) ~src:(dummy_loc,GoalEvar) ty in
       clenv_assign mv evar {clenv with evd=evd})
     clenv
     dep_mvs
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 412275c10..a67de715a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -633,7 +633,7 @@ let rec subst_rawconstr subst raw =
 	if ref' == ref then raw else
 	  RHole (loc,InternalHole)
   | RHole (loc, (BinderType _ | QuestionMark _ | CasesType |
-      InternalHole | TomatchTypeParameter _)) -> raw
+      InternalHole | TomatchTypeParameter _ | GoalEvar)) -> raw
 
   | RCast (loc,r1,k) -> 
       (match k with 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 99aa440b3..349cfb063 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -415,6 +415,8 @@ let need_restriction k args = not (array_for_all (closedn k) args)
  * false. The problem is that we won't get the right error message.
  *)
 
+exception NotClean of constr
+
 let real_clean env isevars ev evi args rhs =
   let evd = ref isevars in
   let subst = List.map (fun (x,y) -> (y,mkVar x)) (list_uniquize args) in
@@ -425,7 +427,7 @@ let real_clean env isevars ev evi args rhs =
  	 else
 	   (* Flex/Rel problem: unifiable as a pattern iff Rel in ev scope *)
 	   (try List.assoc (mkRel (i-k)) subst 
-	    with Not_found -> if rigid then raise Exit else t)
+	    with Not_found -> if rigid then raise (NotClean t) else t)
       | Evar (ev,args) ->
           if Evd.is_defined_evar !evd (ev,args) then
             subs rigid k (existential_value (evars_of !evd) (ev,args))
@@ -451,7 +453,7 @@ let real_clean env isevars ev evi args rhs =
 		 or List.exists (fun (id',_,_) -> id=id') (evar_context evi)
 	     *)
              then t
-             else raise Exit)
+             else raise (NotClean t))
                
       | _ ->
 	  (* Flex/Rigid problem (or assimilated if not normal): we "imitate" *)
@@ -461,8 +463,8 @@ let real_clean env isevars ev evi args rhs =
   let rhs = whd_beta rhs (* heuristic *) in
   let body = 
     try subs true 0 rhs
-    with Exit -> 
-      error_not_clean env (evars_of !evd) ev rhs (evar_source ev !evd) in
+    with NotClean t -> 
+      error_not_clean env (evars_of !evd) ev t (evar_source ev !evd) in
   (!evd,body)
 
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 439f46264..6b75e15f0 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -378,6 +378,7 @@ type hole_kind =
   | CasesType
   | InternalHole
   | TomatchTypeParameter of inductive * int
+  | GoalEvar
 
 type conv_pb = Reduction.conv_pb
 type evar_constraint = conv_pb * Environ.env * constr * constr
@@ -395,6 +396,9 @@ let subst_evar_defs_light sub evd =
 
 let create_evar_defs sigma =
   { evars=sigma; conv_pbs=[]; history=[]; metas=Metamap.empty }
+let create_goal_evar_defs sigma =
+  let h = fold (fun mv _ l -> (mv,(dummy_loc,GoalEvar))::l) sigma [] in
+  { evars=sigma; conv_pbs=[]; history=h; metas=Metamap.empty }
 let evars_of d = d.evars
 let evars_reset_evd evd d = {d with evars = evd}
 let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap}
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 4375f5471..735889034 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -133,7 +133,8 @@ type evar_defs
 val subst_evar_defs_light : substitution -> evar_defs -> evar_defs
 
 (* create an [evar_defs] with empty meta map: *)
-val create_evar_defs : evar_map -> evar_defs
+val create_evar_defs      : evar_map -> evar_defs
+val create_goal_evar_defs : evar_map -> evar_defs
 val evars_of         : evar_defs -> evar_map
 val evars_reset_evd  : evar_map ->  evar_defs -> evar_defs
 
@@ -145,6 +146,7 @@ type hole_kind =
   | CasesType
   | InternalHole
   | TomatchTypeParameter of inductive * int
+  | GoalEvar
 val is_defined_evar :  evar_defs -> existential -> bool
 val is_undefined_evar :  evar_defs -> constr -> bool
 val undefined_evars : evar_defs -> evar_defs
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4116445e1..4624456a8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -312,7 +312,8 @@ let applyHead env evd n c  =
     else 
       match kind_of_term (whd_betadeltaiota env (evars_of evd) cty) with
         | Prod (_,c1,c2) ->
-            let (evd',evar) = Evarutil.new_evar evd env c1 in
+            let (evd',evar) = 
+	      Evarutil.new_evar evd env ~src:(dummy_loc,GoalEvar) c1 in
 	    apprec (n-1) (mkApp(c,[|evar|])) (subst1 evar c2) evd'
 	| _ -> error "Apply_Head_Then"
   in 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index db94fad14..785316d56 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -89,7 +89,7 @@ let e_res_pf clenv gls =
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
 let unifyTerms m n gls = 
   let env = pf_env gls in
-  let evd = create_evar_defs (project gls) in
+  let evd = create_goal_evar_defs (project gls) in
   let evd' = Unification.w_unify false env CONV m n evd in
   tclIDTAC {it = gls.it; sigma = evars_of evd'}
 
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index f0e2fef68..226cb3f01 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -51,6 +51,6 @@ let instantiate_pf_com n com pfts =
   in 
   let env = Evd.evar_env evi in
   let rawc = Constrintern.intern_constr sigma env com in 
-  let evd = create_evar_defs sigma in
+  let evd = create_goal_evar_defs sigma in
   let evd' = w_refine sp rawc evd in
     change_constraints_pftreestate (evars_of evd') pfts
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5e831dd4c..d664013c7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -70,7 +70,7 @@ let with_check = Options.with_option check
    (instead of iterating on the list of identifier to be removed, which
    forces the user to give them in order). *)
 let clear_hyps sigma ids gl =
-  let evd = ref (Evd.create_evar_defs sigma) in
+  let evd = ref (Evd.create_goal_evar_defs sigma) in
   let ngl = Evarutil.clear_hyps_in_evi evd gl ids in
     (ngl, evars_of !evd)
 
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index d50477316..62ed700a2 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -24,7 +24,7 @@ open Rawterm
 let absurd c gls =
   let env = pf_env gls and sigma = project gls in
   let _,j = Coercion.Default.inh_coerce_to_sort dummy_loc env
-    (Evd.create_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in
+    (Evd.create_goal_evar_defs sigma) (Retyping.get_judgment_of env sigma c) in
   let c = j.Environ.utj_val in
   (tclTHENS
      (tclTHEN (elim_type (build_coq_False ())) (cut c)) 
diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml
index 28fc640d1..74ffc0a9c 100644
--- a/tactics/decl_proof_instr.ml
+++ b/tactics/decl_proof_instr.ml
@@ -83,7 +83,7 @@ Please \"suppose\" something or \"end\" it now."
       | _ -> ()
 
 let mk_evd metalist gls =
-  let evd0= create_evar_defs (sig_sig gls) in
+  let evd0= create_goal_evar_defs (sig_sig gls) in
   let add_one (meta,typ) evd = 
     meta_declare meta typ evd in
     List.fold_right add_one metalist evd0
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8c8716110..c5b7aeedf 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -650,7 +650,7 @@ let minimal_free_rels env sigma (c,cty) =
 
 let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
   let { intro = exist_term } = find_sigma_data sort_of_ty in 
-  let isevars = ref (Evd.create_evar_defs sigma) in
+  let isevars = ref (Evd.create_goal_evar_defs sigma) in
   let rec sigrec_clausal_form siglen p_i =
     if siglen = 0 then
       (* is the default value typable with the expected type *)
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index f3454b711..784455ff0 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -51,7 +51,7 @@ let instantiate n rawc ido gl =
       error "not enough uninstantiated existential variables";
     if n <= 0 then error "incorrect existential variable index";
     let ev,_ =  destEvar (List.nth evl (n-1)) in
-    let evd' = w_refine ev rawc (create_evar_defs sigma)  in
+    let evd' = w_refine ev rawc (create_goal_evar_defs sigma)  in
       Refiner.tclEVARS (evars_of evd') gl
 	
 (*
@@ -68,7 +68,7 @@ let instantiate_tac = function
 *)
 
 let let_evar name typ gls =
-  let evd = Evd.create_evar_defs gls.sigma in
+  let evd = Evd.create_goal_evar_defs gls.sigma in
   let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in
   Refiner.tclTHEN (Refiner.tclEVARS (evars_of evd'))
     (Tactics.letin_tac true name evar nowhere) gls
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 7e45efe94..e25ff99e0 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -312,31 +312,32 @@ let explain_occur_check env ev rhs =
   pt ++ spc () ++ str "that would depend on itself."
 
 let explain_hole_kind env = function
-  | QuestionMark _ -> str "a term for this placeholder"
+  | QuestionMark _ -> str "this placeholder"
   | CasesType ->
       str "the type of this pattern-matching problem"
   | BinderType (Name id) ->
-      str "a type for " ++ Nameops.pr_id id
+      str "the type of " ++ Nameops.pr_id id
   | BinderType Anonymous ->
-      str "a type for this anonymous binder"
+      str "the type of this anonymous binder"
   | ImplicitArg (c,(n,ido)) ->
       let id = out_some ido in
-      str "an instance for the implicit parameter " ++
+      str "the implicit parameter " ++
       pr_id id ++ spc () ++ str "of" ++
       spc () ++ Nametab.pr_global_env Idset.empty c
   | InternalHole ->
-      str "a term for an internal placeholder"
+      str "an internal placeholder"
   | TomatchTypeParameter (tyi,n) ->
       str "the " ++ nth n ++
       str " argument of the inductive type (" ++ pr_inductive env tyi ++
       str ") of this term"
+  | GoalEvar ->
+      str "an existential variable"
 
 let explain_not_clean env ev t k =
   let env = make_all_name_different env in
-  let c = mkRel (Intset.choose (free_rels t)) in
   let id = Evd.string_of_existential ev in
-  let var = pr_lconstr_env env c in
-  str "Tried to define " ++ explain_hole_kind env k ++
+  let var = pr_lconstr_env env t in
+  str "Tried to instantiate " ++ explain_hole_kind env k ++
   str " (" ++ str id ++ str ")" ++ spc () ++
   str "with a term using variable " ++ var ++ spc () ++
   str "which is not in its scope."