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

6 files changed, 20 insertions, 10 deletions

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 5f4293abf1..1c35f9f720 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 412275c108..a67de715a8 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 99aa440b3f..349cfb0633 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 439f462642..6b75e15f0e 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 4375f54714..7358890343 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 4116445e16..4624456a8f 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