Improving a few error messages in Ltac interpretation

- improving error message when a reference to unfold is not found
- repairing anomaly when an evaluable reference exists at
  internalisation-time but not at run time, and similarly for an
  arbitrary term (but the latter is new from 8.3 because of the new
  use of retyping instead of understand for typing Ltac values)

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

4 files changed, 40 insertions, 8 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8898e5989a..7017edaf28 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -249,6 +249,11 @@ module Pretyping_F (Coercion : Coercion.S) = struct
 	str " depends on pattern variable name " ++ pr_id id ++
 	str " which is not bound in current context.")
 
+  let protected_get_type_of env sigma c =
+    try Retyping.get_type_of env sigma c
+    with Anomaly _ ->
+      errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.")
+
   let pretype_id loc env sigma (lvar,unbndltacvars) id =
     (* Look for the binder of [id] *)
     try
@@ -260,7 +265,7 @@ module Pretyping_F (Coercion : Coercion.S) = struct
       let (ids,c) = List.assoc id lvar in
       let subst = List.map (invert_ltac_bound_name env id) ids in
       let c = substl subst c in
-      { uj_val = c; uj_type = Retyping.get_type_of env sigma c }
+      { uj_val = c; uj_type = protected_get_type_of env sigma c }
     with Not_found ->
     (* Check if [id] is a section or goal variable *)
     try
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1957f04751..f067141a8b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -395,8 +395,10 @@ let intern_ltac_variable ist = function
       raise Not_found
 
 let intern_constr_reference strict ist = function
-  | Ident (_,id) when (not strict & find_hyp id ist) or find_ctxvar id ist ->
-      RVar (dloc,id), None
+  | Ident (_,id) as r when not strict & find_hyp id ist ->
+      RVar (dloc,id), Some (CRef r)
+  | Ident (_,id) as r when find_ctxvar id ist ->
+      RVar (dloc,id), if strict then None else Some (CRef r)
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
       RRef (loc,locate_global_with_alias lqid), if strict then None else Some (CRef r)
@@ -558,9 +560,10 @@ let intern_evaluable_reference_or_by_notation ist = function
 (* Globalize a reduction expression *)
 let intern_evaluable ist = function
   | AN (Ident (loc,id)) when find_ltacvar id ist -> ArgVar (loc,id)
-  | AN (Ident (_,id)) when
-      (not !strict_check & find_hyp id ist) or find_ctxvar id ist ->
-      ArgArg (EvalVarRef id, None)
+  | AN (Ident (loc,id)) when not !strict_check & find_hyp id ist ->
+      ArgArg (EvalVarRef id, Some (loc,id))
+  | AN (Ident (loc,id)) when find_ctxvar id ist ->
+      ArgArg (EvalVarRef id, if !strict_check then None else Some (loc,id))
   | r ->
       let e = intern_evaluable_reference_or_by_notation ist r in
       let na = short_name r in
@@ -1132,7 +1135,8 @@ let interp_hyp ist gl (loc,id as locid) =
   with Not_found ->
   (* Then look if bound in the proof context at calling time *)
   if is_variable env id then id
-  else user_err_loc (loc,"eval_variable",pr_id id ++ str " not found.")
+  else user_err_loc (loc,"eval_variable",
+    str "No such hypothesis: " ++ pr_id id ++ str ".")
 
 let hyp_list_of_VList env = function
   | VList l -> List.map (coerce_to_hyp env) l
@@ -1204,7 +1208,7 @@ let interp_evaluable ist env = function
        with Not_found ->
        match r with
        | EvalConstRef _ -> r
-       | _ -> Pretype_errors.error_var_not_found_loc loc id)
+       | _ -> error_global_not_found_loc (loc,qualid_of_ident id))
   | ArgArg (r,None) -> r
   | ArgVar locid ->
       interp_ltac_var (coerce_to_evaluable_ref env) ist (Some env) locid
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index bbaeb08992..32c6d14311 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -266,3 +266,18 @@ reflexivity.
 f_non_linear ((forall x y, x+y = 0) -> (forall y x, y+x = 0)) (* should fail *)
 || exact I.
 Qed.
+
+(* Test regular failure when clear/intro breaks soundness of the
+   interpretation of terms in current environment *)
+
+Ltac g y := clear y; assert (y=y).
+Goal forall x:nat, True.
+intro x.
+Fail g x.
+Abort.
+
+Ltac h y := assert (y=y).
+Goal forall x:nat, True.
+intro x.
+Fail clear x; f x.
+Abort.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 47ca0836b5..5649e2f712 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -13,3 +13,11 @@ Goal EQ nat 0 0.
 Hint Unfold EQ.
 auto.
 Qed.
+
+(* Check regular failure when statically existing ref does not exist
+   any longer at run time *)
+
+Goal let x := 0 in True.
+intro x.
+Fail (clear x; unfold x).
+Abort.