From bc1ddb1081dd44887cb2f8b33937138cb1e1658c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 11 Sep 2010 19:19:04 +0000
Subject: 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
---
 pretyping/pretyping.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3