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

1 files changed, 6 insertions, 1 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