diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -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) = |