From 099ac51a6c03a5ac7178b4ea616763dac73a484e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 12 Feb 2004 20:40:10 +0000
Subject: Plus d'explicitation d'un message d'erreur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5330 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tacinterp.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3ffc182f55..809e5a2300 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -985,7 +985,8 @@ let eval_ident ist id =
       (* c is then expected not to belong to the proof context *)
       (* would be checkable if env were known from eval_ident *)
       destVar c
-  | _ -> user_err_loc(loc,"eval_ident",str "should be bound to an identifier")
+  | _ -> user_err_loc(loc,"eval_ident", str "An ltac name (" ++ pr_id id ++ 
+         str ") should have been bound to an identifier")
   with Not_found -> id
 
 let eval_integer lfun (loc,id) =
-- 
cgit v1.2.3