diff options
| author | herbelin | 2004-02-12 20:40:10 +0000 |
|---|---|---|
| committer | herbelin | 2004-02-12 20:40:10 +0000 |
| commit | 099ac51a6c03a5ac7178b4ea616763dac73a484e (patch) | |
| tree | ca2e9862ce4703aba2fe100f171512c0933c98f3 | |
| parent | f03055b760f79e4e5a1efb4706823a2735a24048 (diff) | |
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
| -rw-r--r-- | tactics/tacinterp.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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) = |