aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tactics/tacinterp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 46428236c5..3012cbae2f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1004,7 +1004,7 @@ let try_interp_ltac_var coerce ist env (loc,id) =
let interp_ltac_var coerce ist env locid =
try try_interp_ltac_var coerce ist env locid
- with Not_found -> anomaly "Detected as ltac var at interning time"
+ with Not_found -> anomaly ("Detected '" ^ (string_of_id (snd locid)) ^ "' as ltac var at interning time")
(* Interprets an identifier which must be fresh *)
let coerce_to_ident fresh env = function