From bece6859bf6ee3e652c2e6e5596312580edc7e1d Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 18 Jul 2020 11:45:40 +0200
Subject: Clarify the Ltac2 invalid identifier message.

---
 user-contrib/Ltac2/tac2quote.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/user-contrib/Ltac2/tac2quote.ml b/user-contrib/Ltac2/tac2quote.ml
index 3aea2bea8d..b346b3ee5c 100644
--- a/user-contrib/Ltac2/tac2quote.ml
+++ b/user-contrib/Ltac2/tac2quote.ml
@@ -88,7 +88,8 @@ let inj_wit ?loc wit x =
 let of_variable {loc;v=id} =
   let qid = Libnames.qualid_of_ident ?loc id in
   if Tac2env.is_constructor qid then
-    CErrors.user_err ?loc (str "Invalid identifier")
+    CErrors.user_err ?loc (str "Invalid identifier" ++ spc () ++ Id.print id ++
+      spc () ++ str "classifying as an Ltac2 constructor")
   else CAst.make ?loc @@ CTacRef (RelId qid)
 
 let of_anti f = function
-- 
cgit v1.2.3