diff options
Diffstat (limited to 'tactics')
| -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 8b0632c199..876f13c33d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1210,7 +1210,8 @@ let coerce_to_int = function let interp_int ist locid = try try_interp_ltac_var coerce_to_int ist None locid - with Not_found -> user_err_loc(fst locid,"interp_int",str "Unbound variable") + with Not_found -> user_err_loc(fst locid,"interp_int", + str "Unbound variable" ++ pr_id (snd locid)) let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid |